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