|
|
|
|
Venues (Conferences, Journals, ...)
|
|
|
GrowBag graphs for keyword ? (Num. hits/coverage)
Group by:
No Growbag Graphs found.
|
|
|
|
|
Results
Found 21 publication records. Showing 21 according to the selection in the facets
| Hits ?▲ |
Authors |
Title |
Venue |
Year |
Link |
Author keywords |
| 1 | Mark Adams |
The Common HOL Platform.  |
PxTP@CADE  |
2015 |
DBLP DOI BibTeX RDF |
|
| 1 | Ali Assaf 0002, Raphaël Cauderlier |
Mixing HOL and Coq in Dedukti (Extended Abstract). |
PxTP@CADE |
2015 |
DBLP DOI BibTeX RDF |
|
| 1 | Raphaël Cauderlier, Pierre Halmagrand |
Checking Zenon Modulo Proofs in Dedukti. |
PxTP@CADE |
2015 |
DBLP DOI BibTeX RDF |
|
| 1 | Giselle Reis |
Importing SMT and Connection proofs as expansion trees. |
PxTP@CADE |
2015 |
DBLP DOI BibTeX RDF |
|
| 1 | Ali Assaf 0002, Guillaume Burel |
Translating HOL to Dedukti. |
PxTP@CADE |
2015 |
DBLP DOI BibTeX RDF |
|
| 1 | Cezary Kaliszyk, Andrei Paskevich (eds.) |
Proceedings Fourth Workshop on Proof eXchange for Theorem Proving, PxTP 2015, Berlin, Germany, August 2-3, 2015. |
PxTP@CADE |
2015 |
DBLP DOI BibTeX RDF |
|
| 1 | Quentin Heath, Dale Miller 0001 |
A framework for proof certificates in finite state exploration. |
PxTP@CADE |
2015 |
DBLP DOI BibTeX RDF |
|
| 1 | Christoph Benzmüller, Maximilian Claus, Nik Sultana |
Systematic Verification of the Modal Logic Cube in Isabelle/HOL. |
PxTP@CADE |
2015 |
DBLP DOI BibTeX RDF |
|
| 1 | Jasmin Christian Blanchette, Josef Urban (eds.) |
Third International Workshop on Proof Exchange for Theorem Proving, PxTP 2013, Lake Placid, NY, USA, June 9-10, 2013 |
PxTP@CADE |
2013 |
DBLP BibTeX RDF |
|
| 1 | Thomas C. Hales |
External Tools for the Formal Proof of the Kepler Conjecture. |
PxTP@CADE |
2013 |
DBLP DOI BibTeX RDF |
|
| 1 | Steffen Juilf Smolka, Jasmin Christian Blanchette |
Robust, Semi-Intelligible Isabelle Proofs from ATP Proofs. |
PxTP@CADE |
2013 |
DBLP DOI BibTeX RDF |
|
| 1 | Ramana Kumar |
Challenges in Using OpenTheory to Transport Harrison's HOL Model from HOL Light to HOL4. |
PxTP@CADE |
2013 |
DBLP DOI BibTeX RDF |
|
| 1 | Chantal Keller |
Extended Resolution as Certificates for Propositional Logic. |
PxTP@CADE |
2013 |
DBLP DOI BibTeX RDF |
|
| 1 | Nada Habli, Amy P. Felty |
Translating Higher-Order Specifications to Coq Libraries Supporting Hybrid Proofs. |
PxTP@CADE |
2013 |
DBLP DOI BibTeX RDF |
|
| 1 | Jasmin Christian Blanchette |
Redirecting Proofs by Contradiction. |
PxTP@CADE |
2013 |
DBLP DOI BibTeX RDF |
|
| 1 | Cezary Kaliszyk, Thomas Sternagel |
Initial Experiments on Deriving a Complete HOL Simplification Set. |
PxTP@CADE |
2013 |
DBLP DOI BibTeX RDF |
|
| 1 | Cezary Kaliszyk, Josef Urban |
Stronger Automation for Flyspeck by Feature Weighting and Strategy Evolution. |
PxTP@CADE |
2013 |
DBLP DOI BibTeX RDF |
|
| 1 | Guillaume Burel |
A Shallow Embedding of Resolution and Superposition Proofs into the λΠ-Calculus Modulo. |
PxTP@CADE |
2013 |
DBLP DOI BibTeX RDF |
|
| 1 | Zakaria Chihani, Dale Miller 0001, Fabien Renaud |
Checking Foundational Proof Certificates for First-Order Logic (Extended Abstract). |
PxTP@CADE |
2013 |
DBLP DOI BibTeX RDF |
|
| 1 | Christoph Benzmüller, Nik Sultana |
LEO-II Version 1.5. |
PxTP@CADE |
2013 |
DBLP DOI BibTeX RDF |
|
| 1 | Chad E. Brown, Christine Rizkallah |
From Classical Extensional Higher-Order Tableau to Intuitionistic Intentional Natural Deduction. |
PxTP@CADE |
2013 |
DBLP DOI BibTeX RDF |
|
Displaying result #1 - #21 of 21 (100 per page; Change: )
|
|
![[Valid RSS]](Pics/valid-rss.png "Validate my RSS feed")
data released under the ODC-BY 1.0 license