Back to Search
Start Over
Superposition with lambdas
- Source :
- Journal of Automated Reasoning, 65(7), 893-940. Springer Netherlands, Bentkamp, A, Blanchette, J, Tourret, S, Vukmirović, P & Waldmann, U 2019, Superposition with lambdas . in P Fontaine (ed.), Automated Deduction – CADE 2019 : 27th International Conference on Automated Deduction, Natal, Brazil, August 27–30, 2019, Proceedings . Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), vol. 11716 LNAI, Springer, pp. 55-73, 27th International Conference on Automated Deduction, CADE 2019, Natal, Brazil, 27/08/19 . https://doi.org/10.1007/978-3-030-29436-6_4, Lecture Notes in Computer Science ISBN: 9783030294359, CADE, Automated Deduction – CADE 27-27th International Conference on Automated Deduction, Natal, Brazil, August 27–30, 2019, Proceedings, Journal of Automated Reasoning, Journal of Automated Reasoning, Springer Verlag, 2021, 65 (7), pp.893-940. ⟨10.1007/s10817-021-09595-y⟩, Bentkamp, A, Blanchette, J, Tourret, S, Vukmirović, P & Waldmann, U 2021, ' Superposition with Lambdas ', Journal of Automated Reasoning, vol. 65, no. 7, pp. 893-940 . https://doi.org/10.1007/s10817-021-09595-y, CADE-27-The 27th International Conference on Automated Deduction, CADE-27-The 27th International Conference on Automated Deduction, Aug 2019, Natal, Brazil. pp.55-73, ⟨10.1007/978-3-030-29436-6_4⟩, Automated Deduction – CADE 2019: 27th International Conference on Automated Deduction, Proceedings, 55-73, STARTPAGE=55;ENDPAGE=73;TITLE=Automated Deduction – CADE 2019, Lecture Notes in Computer Science, Lecture Notes in Computer Science-Automated Deduction – CADE 27, Journal of Automated Reasoning, 2021, 65 (7), pp.893-940. ⟨10.1007/s10817-021-09595-y⟩
- Publication Year :
- 2019
-
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.
- Subjects :
- FOS: Computer and information sciences
Computer Science - Logic in Computer Science
Logic in computer science
Unification
Computer Science - Artificial Intelligence
02 engineering and technology
0102 computer and information sciences
Gas meter prover
01 natural sciences
Higher-order logic
Anonymous function
Refutational completeness
Fragment (logic)
F.4.1
I.2.3
Artificial Intelligence
Computer Science::Logic in Computer Science
Superposition calculus
0202 electrical engineering, electronic engineering, information engineering
0101 mathematics
Rule of inference
Mathematics
Discrete mathematics
010102 general mathematics
[INFO.INFO-LO]Computer Science [cs]/Logic in Computer Science [cs.LO]
020207 software engineering
16. Peace & justice
Logic in Computer Science (cs.LO)
Artificial Intelligence (cs.AI)
TheoryofComputation_MATHEMATICALLOGICANDFORMALLANGUAGES
Computational Theory and Mathematics
010201 computation theory & mathematics
Completeness (logic)
TheoryofComputation_LOGICSANDMEANINGSOFPROGRAMS
Software
Subjects
Details
- Language :
- English
- ISBN :
- 978-3-030-29435-9
978-3-030-29436-6 - ISSN :
- 03029743, 01687433, 15730670, and 16113349
- ISBNs :
- 9783030294359 and 9783030294366
- Database :
- OpenAIRE
- Journal :
- Automated Deduction – CADE 2019
- Accession number :
- edsair.doi.dedup.....47cb97cb39d714e225a6d4fba246a173
- Full Text :
- https://doi.org/10.1007/978-3-030-29436-6_4