Superposition for Lambda-Free Higher-Order Logic

Autor: Alexander Bentkamp, Jasmin Blanchette, Simon Cruanes, Uwe Waldmann

Publikováno v: Logical Methods in Computer Science, Vol Volume 17, Issue 2 (2021)

We introduce refutationally complete superposition calculi for intentional and extensional clausal $\lambda$-free higher-order logic, two formalisms that allow partial application and applied variables. The calculi are parameterized by a term order t

Externí odkaz: https://doaj.org/article/74edf34adb99427592d3b893e634da31

Extending Nunchaku to Dependent Type Theory

Autor: Simon Cruanes, Jasmin Christian Blanchette

Publikováno v: Electronic Proceedings in Theoretical Computer Science, Vol 210, Iss Proc. HaTT 2016, Pp 3-12 (2016)

Nunchaku is a new higher-order counterexample generator based on a sequence of transformations from polymorphic higher-order logic to first-order logic. Unlike its predecessor Nitpick for Isabelle, it is designed as a stand-alone tool, with frontends

Externí odkaz: https://doaj.org/article/b7a9953e270949af90abbf581487e2a5

Extending a Brainiac Prover to Lambda-Free Higher-Order Logic

Autor: Petar Vukmirović, Simon Cruanes, Stephan Schulz, Jasmin Christian Blanchette

Publikováno v: Tools and Algorithms for the Construction and Analysis of Systems ISBN: 9783030174613
TACAS (1)
TACAS 2019-25th International Conference on Tools and Algorithms for the Construction and Analysis of Systems
TACAS 2019-25th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, Apr 2019, Prague, Czech Republic. pp.192-210
Vukmirović, P, Blanchette, J, Cruanes, S & Schulz, S 2022, ' Extending a brainiac prover to lambda-free higher-order logic ', International Journal on Software Tools for Technology Transfer, vol. 24, no. 1, pp. 67-87 . https://doi.org/10.1007/s10009-021-00639-7
International Journal on Software Tools for Technology Transfer
International Journal on Software Tools for Technology Transfer, 2022, 24 (1), pp.67-87. ⟨10.1007/s10009-021-00639-7⟩
International Journal on Software Tools for Technology Transfer (STTT)
Tools and Algorithms for the Construction and Analysis of Systems
Lecture Notes in Computer Science
Tools and Algorithms for the Construction and Analysis of Systems: 25th International Conference, TACAS 2019, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2019, Prague, Czech Republic, April 6–11, 2019, Proceedings, Part I, 1, 192-210
Vukmirović, P, Blanchette, J C, Cruanes, S & Schulz, S 2019, Extending a brainiac prover to lambda-free higher-order logic . in L Zhang & T Vojnar (eds), Tools and Algorithms for the Construction and Analysis of Systems : 25th International Conference, TACAS 2019, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2019, Prague, Czech Republic, April 6–11, 2019, Proceedings, Part I . vol. 1, Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), vol. 11427 LNCS, Springer Verlag, pp. 192-210, 25th International Conference on Tools and Algorithms for the Construction and Analysis of Systems conference series, TACAS 2019 held as part of the 22nd European Joint Conferences on Theory and Practice of Software, ETAPS 2019, Prague, Czech Republic, 6/04/19 . https://doi.org/10.1007/978-3-030-17462-0_11
Lecture Notes in Computer Science-Tools and Algorithms for the Construction and Analysis of Systems
Tools and Algorithms for the Construction and Analysis of Systems-25th International Conference, TACAS 2019, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2019, Prague, Czech Republic, April 6–11, 2019, Proceedings, Part I
International Journal on Software Tools for Technology Transfer, 24(1), 67-87. Springer Verlag

Decades of work have gone into developing efficient proof calculi, data structures, algorithms, and heuristics for first-order automatic theorem proving. Higher-order provers lag behind in terms of efficiency. Instead of developing a new higher-order

Externí odkaz: https://explore.openaire.eu/search/publication?articleId=doi_dedup___::3b44dcb82b9c66ccdcad1283d6fa575e
https://doi.org/10.1007/978-3-030-17462-0_11

An Automation-Friendly Set Theory for the B Method

Autor: Simon Cruanes, Guillaume Bury, Pierre-Louis Euvrard, David Delahaye

Publikováno v: 6th International Conference on Abstract State Machines, Alloy, B, TLA, VDM, and Z
ABZ: Abstract State Machines, Alloy, B, TLA, VDM, and Z
ABZ: Abstract State Machines, Alloy, B, TLA, VDM, and Z, Jun 2018, Southampton, United Kingdom. pp.409-414, ⟨10.1007/978-3-319-91271-4_32⟩
Lecture Notes in Computer Science ISBN: 9783319912707
ABZ
ABZ 2018-6th International Conference on Abstract State Machines, Alloy, B, TLA, VDM, and Z
ABZ 2018-6th International Conference on Abstract State Machines, Alloy, B, TLA, VDM, and Z, Jun 2018, Southampton, United Kingdom. pp.409-414, ⟨10.1007/978-3-319-91271-4_32⟩

International audience; We propose an automation-friendly set theory for the B method. This theory is expressed using first order logic extended to poly-morphic types and rewriting. Rewriting is introduced along the lines of deduction modulo theory,

Externí odkaz: https://explore.openaire.eu/search/publication?articleId=doi_dedup___::87f1f25fc6ef4eb1d3fd61729326f814
https://hal.archives-ouvertes.fr/hal-02082755

Language and Proofs for Higher-Order SMT (Work in Progress)

Autor: Daniel El Ouraoui, Pascal Fontaine, Simon Cruanes, Haniel Barbosa, Jasmin Christian Blanchette

Publikováno v: Electronic Proceedings in Theoretical Computer Science, 262(262), 15-22. Open Publishing Association
Electronic Proceedings in Theoretical Computer Science
Electronic Proceedings in Theoretical Computer Science, Vol 262, Iss Proc. PxTP 2017, Pp 15-22 (2017)
Barbosa, H, Blanchette, J C, Cruanes, S, El Ouraoui, D & Fontaine, P 2017, ' Language and Proofs for Higher-Order SMT (Work in Progress) ', Electronic Proceedings in Theoretical Computer Science, vol. 262, no. 262, pp. 15-22 . https://doi.org/10.4204/EPTCS.262.3
PxTP

Satisfiability modulo theories (SMT) solvers have throughout the years been able to cope with increasingly expressive formulas, from ground logics to full first-order logic modulo theories. Nevertheless, higher-order logic within SMT is still little

Externí odkaz: https://explore.openaire.eu/search/publication?articleId=doi_dedup___::5febcbb470d25ba8c6b33c2b236ef7ed
http://arxiv.org/abs/1712.01486