|
|
|
|
Venues (Conferences, Journals, ...)
|
|
|
GrowBag graphs for keyword ? (Num. hits/coverage)
Group by:
No Growbag Graphs found.
|
|
|
|
|
Results
Found 36 publication records. Showing 36 according to the selection in the facets
| Hits ?▲ |
Authors |
Title |
Venue |
Year |
Link |
Author keywords |
| 1 | Hans-Jörg Schurr, Mathias Fleury, Haniel Barbosa, Pascal Fontaine |
Alethe: Towards a Generic SMT Proof Format (extended abstract).  |
PxTP  |
2021 |
DBLP DOI BibTeX RDF |
|
| 1 | Quentin Garchery |
A Framework for Proof-carrying Logical Transformations. |
PxTP |
2021 |
DBLP DOI BibTeX RDF |
|
| 1 | Nicolas Magaud |
Integrating an Automated Prover for Projective Geometry as a New Tactic in the Coq Proof Assistant. |
PxTP |
2021 |
DBLP DOI BibTeX RDF |
|
| 1 | Valentin Blot, Louise Dubois de Prisque, Chantal Keller, Pierre Vial |
General Automation in Coq through Modular Transformations. |
PxTP |
2021 |
DBLP DOI BibTeX RDF |
|
| 1 | Chantal Keller, Mathias Fleury (eds.) |
Proceedings Seventh Workshop on Proof eXchange for Theorem Proving, PxTP 2021, Pittsburg, PA, USA, July 11, 2021. |
PxTP |
2021 |
DBLP DOI BibTeX RDF |
|
| 1 | Maria Paola Bonacina |
Proof Generation in CDSAT. |
PxTP |
2021 |
DBLP DOI BibTeX RDF |
|
| 1 | Stephan Gocht, Jakob Nordström, Ruben Martins |
Certifying CNF Encodings of Pseudo-Boolean Constraints (abstract). |
PxTP |
2021 |
DBLP DOI BibTeX RDF |
|
| 1 | Fadil Kallat, Tristan Schäfer, Anna Vasileva |
CLS-SMT: Bringing Together Combinatory Logic Synthesis and Satisfiability Modulo Theories. |
PxTP |
2019 |
DBLP DOI BibTeX RDF |
|
| 1 | Giselle Reis, Haniel Barbosa (eds.) |
Proceedings Sixth Workshop on Proof eXchange for Theorem Proving, PxTP 2019, Natal, Brazil, August 26, 2019. |
PxTP |
2019 |
DBLP DOI BibTeX RDF |
|
| 1 | Eunice Palmeira da Silva, Fred Freitas, Jens Otten |
Converting ALC Connection Proofs into ALC Sequents. |
PxTP |
2019 |
DBLP DOI BibTeX RDF |
|
| 1 | Mathias Fleury, Hans-Jörg Schurr |
Reconstructing veriT Proofs in Isabelle/HOL. |
PxTP |
2019 |
DBLP DOI BibTeX RDF |
|
| 1 | Mohamed Yacine El Haddad, Guillaume Burel, Frédéric Blanqui |
EKSTRAKTO A tool to reconstruct Dedukti proofs from TSTP files (extended abstract). |
PxTP |
2019 |
DBLP DOI BibTeX RDF |
|
| 1 | Burak Ekici, Arjun Viswanathan, Yoni Zohar, Clark W. Barrett, Cesare Tinelli |
Verifying Bit-vector Invertibility Conditions in Coq (Extended Abstract). |
PxTP |
2019 |
DBLP DOI BibTeX RDF |
|
| 1 | Haniel Barbosa, Jasmin Christian Blanchette, Simon Cruanes, Daniel El Ouraoui, Pascal Fontaine |
Language and Proofs for Higher-Order SMT (Work in Progress). |
PxTP |
2017 |
DBLP DOI BibTeX RDF |
|
| 1 | Gilles Dowek |
Analyzing Individual Proofs as the Basis of Interoperability between Proof Systems. |
PxTP |
2017 |
DBLP DOI BibTeX RDF |
|
| 1 | Catherine Dubois, Bruno Woltzenlogel Paleo (eds.) |
Proceedings of the Fifth Workshop on Proof eXchange for Theorem Proving, PxTP 2017, Brasília, Brazil, 23-24 September 2017. |
PxTP |
2017 |
DBLP BibTeX RDF |
|
| 1 | Robert Y. Lewis |
An Extensible Ad Hoc Interface between Lean and Mathematica. |
PxTP |
2017 |
DBLP DOI BibTeX RDF |
|
| 1 | Tomer Libal, Xaviera Steele |
Determinism in the Certification of UNSAT Proofs. |
PxTP |
2017 |
DBLP DOI BibTeX RDF |
|
| 1 | Dennis Müller 0001, Colin Rothgang, Yufei Liu, Florian Rabe 0001 |
Alignment-based Translations Across Formal Systems Using Interface Theories. |
PxTP |
2017 |
DBLP DOI BibTeX RDF |
|
| 1 | Silvio Ghilardi, Elena Pagani |
Counter Simulations via Higher Order Quantifier Elimination: a preliminary report. |
PxTP |
2017 |
DBLP DOI BibTeX RDF |
|
| 1 | Frédéric Besson, Pierre-Emmanuel Cornilleau, Ronan Saillard |
Walking through the Forest: Fast EUF Proof-Checking Algorithms. |
PxTP |
2012 |
DBLP BibTeX RDF |
|
| 1 | Mathieu Boespflug, Guillaume Burel |
CoqInE: Translating the Calculus of Inductive Constructions into the λΠ-calculus Modulo. |
PxTP |
2012 |
DBLP BibTeX RDF |
|
| 1 | Mathieu Boespflug, Quentin Carbonneaux, Olivier Hermant |
The λΠ-calculus Modulo as a Universal Proof Language. |
PxTP |
2012 |
DBLP BibTeX RDF |
|
| 1 | Cvetan Dunchev, Alexander Leitsch, Tomer Libal, Martin Riener, Mikheil Rukhaia, Daniel Weller 0001, Bruno Woltzenlogel Paleo |
System Feature Description: Importing Refutations into the GAPT Framework. |
PxTP |
2012 |
DBLP BibTeX RDF |
|
| 1 | Aaron Stump, Andrew Reynolds 0001, Cesare Tinelli, Austin Laugesen, Harley Eades III, Corey Oliver, Ruoyu Zhang |
LFSC for SMT Proofs: Work in Progress. |
PxTP |
2012 |
DBLP BibTeX RDF |
|
| 1 | Stephan Merz |
Proofs and Proof Certification in the TLA+ Proof System. |
PxTP |
2012 |
DBLP BibTeX RDF |
|
| 1 | Robert L. Constable |
Proof Assistants and the Dynamic Nature of Formal Theories. |
PxTP |
2012 |
DBLP BibTeX RDF |
|
| 1 | David Pichardie, Tjark Weber (eds.) |
Proceedings of the Second International Workshop on Proof Exchange for Theorem Proving, PxTP 2012, Manchester, UK, June 30, 2012 |
PxTP |
2012 |
DBLP BibTeX RDF |
|
| 1 | Sascha Böhme, Tjark Weber |
Designing Proof Formats: A User's Perspective. |
PxTP |
2011 |
DBLP BibTeX RDF |
|
| 1 | Pascal Fontaine, Aaron Stump (eds.) |
PxTP 2011: First International Workshop on Proof eXchange for Theorem Proving, Wrocław, Poland, August 1, 2011 |
PxTP |
2011 |
DBLP BibTeX RDF |
|
| 1 | Geoff Sutcliffe, Cynthia Chang, Deborah L. McGuinness, Timothy Lebo, Li Ding 0001, Paulo Pinheiro da Silva |
Combining Proofs to form Different Proofs. |
PxTP |
2011 |
DBLP BibTeX RDF |
|
| 1 | Stephan Merz, Hernán Vanzetto |
Towards certification of TLA+ proof obligations with SMT solvers. |
PxTP |
2011 |
DBLP BibTeX RDF |
|
| 1 | Piotr Rudnicki, Josef Urban |
Escape to ATP for Mizar. |
PxTP |
2011 |
DBLP BibTeX RDF |
|
| 1 | David Déharbe, Pascal Fontaine, Bruno Woltzenlogel Paleo |
Quantifier Inference Rules for SMT proofs. |
PxTP |
2011 |
DBLP BibTeX RDF |
|
| 1 | Frédéric Besson, Pierre-Emmanuel Cornilleau, David Pichardie |
A Nelson-Oppen based Proof System using Theory Specific Proof Systems. |
PxTP |
2011 |
DBLP BibTeX RDF |
|
| 1 | Frédéric Besson, Pascal Fontaine, Laurent Théry |
A Flexible Proof Format for SMT: a Proposal. |
PxTP |
2011 |
DBLP BibTeX RDF |
|
Displaying result #1 - #36 of 36 (100 per page; Change: )
|
|
![[Valid RSS]](Pics/valid-rss.png "Validate my RSS feed")
data released under the ODC-BY 1.0 license