Automating free logic in HOL, with an experimental application in category theory

DOI10.1007/s10817-018-09507-7zbMath1434.68639OpenAlexW2908410917MaRDI QIDQ2303232

Dana S. Scott, Christoph Benzmüller

Publication date: 3 March 2020

Published in: Journal of Automated Reasoning (Search for Journal in Brave)

Full work available at URL: http://orbilu.uni.lu/handle/10993/37593

zbMATH Keywords

free logiccategory theoryclassical higher-order logicinteractive and automated theorem proving

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 (2)

Computer-Supported Exploration of a Categorical Axiomatization of Modeloids ⋮ Category theory in Isabelle/HOL as a basis for meta-logical investigation

Uses Software

• Isabelle
• LEO-II
• Nitpick
• Isabelle/HOL
• VAMPIRE
• SPASS
• TPTP
• z3
• HOL
• Satallax
• Sledgehammer
• CVC4
• E Theorem Prover
• Leo-III
• Archive Formal Proofs
• AxiomaticCategoryTheory

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• The higher-order prover \textsc{Leo}-II
• Logic for programming, artificial intelligence, and reasoning. 19th international conference, LPAR-19, Stellenbosch, South Africa, December 14--19, 2013. Proceedings
• Computational logic
• Isabelle/HOL. A proof assistant for higher-order logic
• Extending Sledgehammer with SMT solvers
• Cut-elimination for quantified conditional logic
• Automating Free Logic in Isabelle/HOL
• Satallax: An Automatic Higher-Order Prover
• More SPASS with Isabelle
• Cut-Simulation and Impredicativity
• Higher-order semantics and extensionality
• General models and extensionality
• Nitpick: A Counterexample Generator for Higher-Order Logic Based on a Relational Model Finder
• A formulation of the simple theory of types
• Groups, Categories and Duality

This page was built for publication: Automating free logic in HOL, with an experimental application in category theory