Automating Free Logic in Isabelle/HOL

DOI10.1007/978-3-319-42432-3_6zbMath1434.68638OpenAlexW2490199991MaRDI QIDQ2819197

Christoph Benzmüller, Dana S. Scott

Publication date: 28 September 2016

Published in: Mathematical Software – ICMS 2016 (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/978-3-319-42432-3_6

zbMATH Keywords

free logicmodel findinginteractive and automated theorem provingapplication to category theory

Mathematics Subject Classification ID

Other nonclassical logic (03B60) Mechanization of proofs and logical operations (03B35) Higher-order logic (03B16) Foundations, relations to logic and deductive systems (18A15) Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15)

Related Items (3)

Extensional higher-order paramodulation in Leo-III ⋮ Category theory in Isabelle/HOL as a basis for meta-logical investigation ⋮ Automating free logic in HOL, with an experimental application in category theory

Uses Software

• Isabelle
• Isabelle/HOL
• HOL
• Sledgehammer
• LeoPARD

Cites Work

• Isabelle/HOL. A proof assistant for higher-order logic
• Extending Sledgehammer with SMT solvers
• LeoPARD — A Generic Platform for the Implementation of Higher-Order Reasoners
• Unnamed Item
• Unnamed Item

This page was built for publication: Automating Free Logic in Isabelle/HOL