Current Year
Bentkamp, A., Blanchette, J. C., Tourret, S., Vukmirović, P., & Waldmann, U. (2021). Superposition with Lambdas. Retrieved from https://arxiv.org/abs/2102.00453
(arXiv: 2102.00453) Abstract
We designed a superposition calculus for a clausal fragment of extensional
polymorphic higher-order logic that includes anonymous functions but excludes
Booleans. The inference rules work on $\beta\eta$-equivalence classes of
$\lambda$-terms and rely on higher-order unification to achieve refutational
completeness. We implemented the calculus in the Zipperposition prover and
evaluated it on TPTP and Isabelle benchmarks. The results suggest that
superposition is a suitable basis for higher-order reasoning.
Export
BibTeX
@online{Bentkamp2102.00453,
TITLE = {Superposition with Lambdas},
AUTHOR = {Bentkamp, Alexander and Blanchette, Jasmin Christian and Tourret, Sophie and Vukmirovi{\'c}, Petar and Waldmann, Uwe},
LANGUAGE = {eng},
URL = {https://arxiv.org/abs/2102.00453},
EPRINT = {2102.00453},
EPRINTTYPE = {arXiv},
YEAR = {2021},
MARGINALMARK = {$\bullet$},
ABSTRACT = {We designed a superposition calculus for a clausal fragment of extensional polymorphic higher-order logic that includes anonymous functions but excludes Booleans. The inference rules work on $\beta\eta$-equivalence classes of $\lambda$-terms and rely on higher-order unification to achieve refutational completeness. We implemented the calculus in the Zipperposition prover and evaluated it on TPTP and Isabelle benchmarks. The results suggest that superposition is a suitable basis for higher-order reasoning.},
}
Endnote
%0 Report
%A Bentkamp, Alexander
%A Blanchette, Jasmin Christian
%A Tourret, Sophie
%A Vukmirović, Petar
%A Waldmann, Uwe
%+ External Organizations
Automation of Logic, MPI for Informatics, Max Planck Society
Automation of Logic, MPI for Informatics, Max Planck Society
External Organizations
Automation of Logic, MPI for Informatics, Max Planck Society
%T Superposition with Lambdas :
%G eng
%U http://hdl.handle.net/21.11116/0000-0008-0A44-1
%U https://arxiv.org/abs/2102.00453
%D 2021
%X We designed a superposition calculus for a clausal fragment of extensional
polymorphic higher-order logic that includes anonymous functions but excludes
Booleans. The inference rules work on $\beta\eta$-equivalence classes of
$\lambda$-terms and rely on higher-order unification to achieve refutational
completeness. We implemented the calculus in the Zipperposition prover and
evaluated it on TPTP and Isabelle benchmarks. The results suggest that
superposition is a suitable basis for higher-order reasoning.
%K Computer Science, Logic in Computer Science, cs.LO,Computer Science, Artificial Intelligence, cs.AI
Bromberger, M., Fiori, A., & Weidenbach, C. (2021). Deciding the Bernays-Schoenfinkel Fragment over Bounded Difference Constraints by Simple Clause Learning over Theories. In Verification, Model Checking, and Abstract Interpretation (VMCAI 2021). Copenhagen, Denmark (Online): Springer. doi:10.1007/978-3-030-67067-2_23
Export
BibTeX
@inproceedings{BrombergerFioriWeidenbach_VMCAI2021,
TITLE = {Deciding the {Bernays}-{Schoenfinkel} Fragment over Bounded Difference Constraints by Simple Clause Learning over Theories},
AUTHOR = {Bromberger, Martin and Fiori, Alberto and Weidenbach, Christoph},
LANGUAGE = {eng},
ISBN = {978-3-030-67066-5},
DOI = {10.1007/978-3-030-67067-2_23},
PUBLISHER = {Springer},
YEAR = {2021},
MARGINALMARK = {$\bullet$},
DATE = {2021},
BOOKTITLE = {Verification, Model Checking, and Abstract Interpretation (VMCAI 2021)},
EDITOR = {Henglein, Fritz and Shoham, Sharon and Yakir, Vizel},
PAGES = {511--533},
SERIES = {Lecture Notes in Computer Science},
VOLUME = {12597},
ADDRESS = {Copenhagen, Denmark (Online)},
}
Endnote
%0 Conference Proceedings
%A Bromberger, Martin
%A Fiori, Alberto
%A Weidenbach, Christoph
%+ Automation of Logic, MPI for Informatics, Max Planck Society
Automation of Logic, MPI for Informatics, Max Planck Society
Automation of Logic, MPI for Informatics, Max Planck Society
%T Deciding the Bernays-Schoenfinkel Fragment over Bounded
Difference Constraints by Simple Clause Learning over Theories :
%G eng
%U http://hdl.handle.net/21.11116/0000-0007-7C49-D
%R 10.1007/978-3-030-67067-2_23
%D 2021
%B 22nd International Conference on Verification, Model Checking, and Abstract Interpretation
%Z date of event: 2021-01-17 - 2021-01-19
%C Copenhagen, Denmark (Online)
%B Verification, Model Checking, and Abstract Interpretation
%E Henglein, Fritz; Shoham, Sharon; Yakir, Vizel
%P 511 - 533
%I Springer
%@ 978-3-030-67066-5
%B Lecture Notes in Computer Science
%N 12597
Frohn, F., Hark, M., & Giesl, J. (2021). Termination of Polynomial Loops. In Static Analysis (SAS 2020). Chicago, IL, USA (Online Event): Springer. doi:10.1007/978-3-030-65474-0_5
Export
BibTeX
@inproceedings{Frohn_SAS2020,
TITLE = {Termination of Polynomial Loops},
AUTHOR = {Frohn, Florian and Hark, M. and Giesl, J{\"u}rgen},
LANGUAGE = {eng},
ISBN = {978-3-030-65473-3},
DOI = {10.1007/978-3-030-65474-0_5},
PUBLISHER = {Springer},
YEAR = {2020},
MARGINALMARK = {$\bullet$},
DATE = {2021},
BOOKTITLE = {Static Analysis (SAS 2020)},
EDITOR = {Pichardie, David and Sighireanu, Mihaela},
PAGES = {89--112},
SERIES = {Lecture Notes in Computer Science},
VOLUME = {12389},
ADDRESS = {Chicago, IL, USA (Online Event)},
}
Endnote
%0 Conference Proceedings
%A Frohn, Florian
%A Hark, M.
%A Giesl, Jürgen
%+ Automation of Logic, MPI for Informatics, Max Planck Society
External Organizations
External Organizations
%T Termination of Polynomial Loops :
%G eng
%U http://hdl.handle.net/21.11116/0000-0007-7FE3-B
%R 10.1007/978-3-030-65474-0_5
%D 2021
%B 27th International Static Analysis Symposium
%Z date of event: 2020-11-18 - 2020-11-20
%C Chicago, IL, USA (Online Event)
%B Static Analysis
%E Pichardie, David; Sighireanu, Mihaela
%P 89 - 112
%I Springer
%@ 978-3-030-65473-3
%B Lecture Notes in Computer Science
%N 12389
Tourret, S., & Blanchette, J. C. (2021). A Modular Isabelle Framework for Verifying Saturation Provers. In CPP ’21, 10th ACM SIGPLAN International Conference on Certified Programs and Proofs. Virtual, Denmark: ACM. doi:10.1145/3437992.3439912
Export
BibTeX
@inproceedings{Tourret_CPP2021,
TITLE = {A modular {I}sabelle framework for verifying saturation provers},
AUTHOR = {Tourret, Sophie and Blanchette, Jasmin Christian},
LANGUAGE = {eng},
ISBN = {978-1-4503-8299-1},
DOI = {10.1145/3437992.3439912},
PUBLISHER = {ACM},
YEAR = {2021},
MARGINALMARK = {$\bullet$},
BOOKTITLE = {CPP '21, 10th ACM SIGPLAN International Conference on Certified Programs and Proofs},
EDITOR = {Hri{\c t}cu, C{\u a}t{\u a}lin and Popescu, Andrei},
PAGES = {224--237},
ADDRESS = {Virtual, Denmark},
}
Endnote
%0 Conference Proceedings
%A Tourret, Sophie
%A Blanchette, Jasmin Christian
%+ Automation of Logic, MPI for Informatics, Max Planck Society
External Organizations
%T A Modular Isabelle Framework for Verifying Saturation Provers :
%G eng
%U http://hdl.handle.net/21.11116/0000-0008-0A0F-E
%R 10.1145/3437992.3439912
%D 2021
%B 10th ACM SIGPLAN International Conference on Certified Programs and Proofs
%Z date of event: 2021-01-17 - 2021-01-19
%C Virtual, Denmark
%B CPP '21
%E Hriţcu, Cătălin; Popescu, Andrei
%P 224 - 237
%I ACM
%@ 978-1-4503-8299-1