publication . Article . Other literature type . 2015

The Higher-Order Prover Leo-II

Christoph Benzmüller;
Open Access English
  • Published: 22 Sep 2015
  • Publisher: Springer
  • Country: United Kingdom
Abstract
Leo-II is an automated theorem prover for classical higher-order logic. The prover has pioneered cooperative higher-order-first-order proof automation, it has influenced the development of the TPTP THF infrastructure for higher-order logic, and it has been applied in a wide array of problems. Leo-II may also be called in proof assistants as an external aid tool to save user effort. For this it is crucial that Leo-II returns proof information in a standardised syntax, so that these proofs can eventually be transformed and verified within proof assistants. Recent progress in this direction is reported for the Isabelle/HOL system. The Leo-II project has been suppor...
Subjects
free text keywords: Computational Theory and Mathematics, Software, Artificial Intelligence, Article, Automated theorem proving, Higher-order logic, Proof assistant
Related Organizations
Funded by
EC| THFTPTP
Project
THFTPTP
An Infrastructure for Typed Higher-order Form Automated Theorem Proving
  • Funder: European Commission (EC)
  • Project Code: 219982
  • Funding stream: FP7 | SP3 | PEOPLE
,
RCUK| LEO II: An Effective Higher-Order Theorem Prover
Project
  • Funder: Research Council UK (RCUK)
  • Project Code: EP/D070511/1
  • Funding stream: EPSRC
66 references, page 1 of 5

Álvez, J, Lucio, P, Rigau, G. Adimen-SUMO: reengineering an ontology for first-order reasoning. Int. J. Semantic Web Inf. Syst.. 2012; 8 (4): 80-116 [OpenAIRE] [DOI]

Andrews, PB. On connections and higher order logic. J. Autom. Reason.. 1989; 5 (3): 257-291 [DOI]

Andrews, PB. An Introduction to Mathematical Logic and Type Theory: To Truth Through Proof, Applied Logic Series. 2002

Andrews, PB, Bishop, M, Issar, S, Nesmith, D, Pfenning, F, Xi, H. TPS: a theorem-proving system for classical type theory. J. Autom. Reason.. 1996; 16 (3): 321-353 [DOI]

Backes, J, Brown, CE. Analytic tableaux for higher-order logic with choice. J. Autom. Reason.. 2011; 47 (4): 451-479 [DOI]

6.Benzmüller, C.: A calculus and a system architecture for extensional higher-order resolution. Research Report 97-198, Department of Mathematical Sciences, Carnegie Mellon University, Pittsburgh, USA (1997)

7.Benzmüller, C.: Extensional higher-order paramodulation and RUE-resolution. In: Ganzinger, H. (ed.) Automated Deduction—CADE-16, 16th International Conference on Automated Deduction, Trento, Italy, July 7–10, 1999, Proceedings, no. 1632 in LNCS, pp. 399–413. Springer (1999). doi:10.1007/3-540-48660-7_39

Benzmüller, C. Comparing approaches to resolution based higher-order theorem proving. Synthese. 2002; 133 (1–2): 203-235 [OpenAIRE] [DOI]

9.Benzmüller, C.: Automating access control logic in simple type theory with LEO-II. In: Gritzalis, D., López, J. (eds.) Emerging Challenges for Security, Privacy and Trust, 24th IFIP TC 11 International Information Security Conference, SEC 2009, Pafos, Cyprus, May 18–20, 2009. Proceedings, IFIP, vol. 297, pp. 387–398. Springer (2009). doi:10.1007/978-3-642-01244-0_34

Benzmüller, C. Combining and automating classical and non-classical logics in classical higher-order logic. Ann. Math. Artif. Intell. (CLIMA XI). 2011; 62 (1–2): 103-128 [OpenAIRE] [DOI]

11.Benzmüller, C.: Automating quantified conditional logics in HOL. In: Rossi, F. (ed.) 23r d International Joint Conference on Artificial Intelligence (IJCAI-13), pp. 746–753. Beijing, China (2013a)

12.Benzmüller, C.: A top-down approach to combining logics. In: Proceedings of the 5th International Conference on Agents and Artificial Intelligence (ICAART), pp. 346–351. SciTePress Digital Library, Barcelona (2013b). doi:10.5220/0004324803460351

Benzmüller, C, Delahaye, D, Woltzenlogel Paleo, B. Higher-order automated theorem provers. All about Proofs, Proof for All, Mathematical Logic and Foundations. 2015: 171-214

14.Benzmüller, C., Brown, C.: A structured set of higher-order problems. In: Hurd, J., Melham, T.F. (eds.) Theorem Proving in Higher Order Logics, 18th International Conference, TPHOLs 2005, Oxford, UK, August 22–25, 2005, Proceedings, Springer, no. 3603 in LNCS, pp. 66–81 (2005). doi:10.1007/11541868_5

15.Benzmüller, C., Brown, C.: The curious inference of Boolos in MIZAR and OMEGA. In: Matuszewski, R., Zalewska, A. (eds.) From Insight to Proof - Festschrift in Honour of Andrzej Trybulec, Studies in Logic, Grammar, and Rhetoric, vol. 10(23), pp. 299–388. The University of Bialystok, Polen (2007)

66 references, page 1 of 5
Abstract
Leo-II is an automated theorem prover for classical higher-order logic. The prover has pioneered cooperative higher-order-first-order proof automation, it has influenced the development of the TPTP THF infrastructure for higher-order logic, and it has been applied in a wide array of problems. Leo-II may also be called in proof assistants as an external aid tool to save user effort. For this it is crucial that Leo-II returns proof information in a standardised syntax, so that these proofs can eventually be transformed and verified within proof assistants. Recent progress in this direction is reported for the Isabelle/HOL system. The Leo-II project has been suppor...
Subjects
free text keywords: Computational Theory and Mathematics, Software, Artificial Intelligence, Article, Automated theorem proving, Higher-order logic, Proof assistant
Related Organizations
Funded by
EC| THFTPTP
Project
THFTPTP
An Infrastructure for Typed Higher-order Form Automated Theorem Proving
  • Funder: European Commission (EC)
  • Project Code: 219982
  • Funding stream: FP7 | SP3 | PEOPLE
,
RCUK| LEO II: An Effective Higher-Order Theorem Prover
Project
  • Funder: Research Council UK (RCUK)
  • Project Code: EP/D070511/1
  • Funding stream: EPSRC
66 references, page 1 of 5

Álvez, J, Lucio, P, Rigau, G. Adimen-SUMO: reengineering an ontology for first-order reasoning. Int. J. Semantic Web Inf. Syst.. 2012; 8 (4): 80-116 [OpenAIRE] [DOI]

Andrews, PB. On connections and higher order logic. J. Autom. Reason.. 1989; 5 (3): 257-291 [DOI]

Andrews, PB. An Introduction to Mathematical Logic and Type Theory: To Truth Through Proof, Applied Logic Series. 2002

Andrews, PB, Bishop, M, Issar, S, Nesmith, D, Pfenning, F, Xi, H. TPS: a theorem-proving system for classical type theory. J. Autom. Reason.. 1996; 16 (3): 321-353 [DOI]

Backes, J, Brown, CE. Analytic tableaux for higher-order logic with choice. J. Autom. Reason.. 2011; 47 (4): 451-479 [DOI]

6.Benzmüller, C.: A calculus and a system architecture for extensional higher-order resolution. Research Report 97-198, Department of Mathematical Sciences, Carnegie Mellon University, Pittsburgh, USA (1997)

7.Benzmüller, C.: Extensional higher-order paramodulation and RUE-resolution. In: Ganzinger, H. (ed.) Automated Deduction—CADE-16, 16th International Conference on Automated Deduction, Trento, Italy, July 7–10, 1999, Proceedings, no. 1632 in LNCS, pp. 399–413. Springer (1999). doi:10.1007/3-540-48660-7_39

Benzmüller, C. Comparing approaches to resolution based higher-order theorem proving. Synthese. 2002; 133 (1–2): 203-235 [OpenAIRE] [DOI]

9.Benzmüller, C.: Automating access control logic in simple type theory with LEO-II. In: Gritzalis, D., López, J. (eds.) Emerging Challenges for Security, Privacy and Trust, 24th IFIP TC 11 International Information Security Conference, SEC 2009, Pafos, Cyprus, May 18–20, 2009. Proceedings, IFIP, vol. 297, pp. 387–398. Springer (2009). doi:10.1007/978-3-642-01244-0_34

Benzmüller, C. Combining and automating classical and non-classical logics in classical higher-order logic. Ann. Math. Artif. Intell. (CLIMA XI). 2011; 62 (1–2): 103-128 [OpenAIRE] [DOI]

11.Benzmüller, C.: Automating quantified conditional logics in HOL. In: Rossi, F. (ed.) 23r d International Joint Conference on Artificial Intelligence (IJCAI-13), pp. 746–753. Beijing, China (2013a)

12.Benzmüller, C.: A top-down approach to combining logics. In: Proceedings of the 5th International Conference on Agents and Artificial Intelligence (ICAART), pp. 346–351. SciTePress Digital Library, Barcelona (2013b). doi:10.5220/0004324803460351

Benzmüller, C, Delahaye, D, Woltzenlogel Paleo, B. Higher-order automated theorem provers. All about Proofs, Proof for All, Mathematical Logic and Foundations. 2015: 171-214

14.Benzmüller, C., Brown, C.: A structured set of higher-order problems. In: Hurd, J., Melham, T.F. (eds.) Theorem Proving in Higher Order Logics, 18th International Conference, TPHOLs 2005, Oxford, UK, August 22–25, 2005, Proceedings, Springer, no. 3603 in LNCS, pp. 66–81 (2005). doi:10.1007/11541868_5

15.Benzmüller, C., Brown, C.: The curious inference of Boolos in MIZAR and OMEGA. In: Matuszewski, R., Zalewska, A. (eds.) From Insight to Proof - Festschrift in Honour of Andrzej Trybulec, Studies in Logic, Grammar, and Rhetoric, vol. 10(23), pp. 299–388. The University of Bialystok, Polen (2007)

66 references, page 1 of 5
Powered by OpenAIRE Research Graph
Any information missing or wrong?Report an Issue