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

DOI10.1007/S10817-018-09507-7MaRDI QIDQ2303232zbMATH OpenOpenAlexFDO

Authors Christoph Benzmüller, Dana Scott

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

category theoryfree logicclassical higher-order logicinteractive and automated theorem proving

Mathematics Subject Classification ID

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

Recommendations

• Automating free logic in Isabelle/HOL
• Towards a readable formalisation of category theory
• Positive Free Higher-Order Logic and Its Automation via a Semantical Embedding
• Automating Proofs in Category Theory
• Nuprl as logical framework for automating proofs in category theory

Cites work

• scientific article; zbMATH DE number 5850137 (Why is no real title available?)
• scientific article; zbMATH DE number 5852776 (Why is no real title available?)
• scientific article; zbMATH DE number 3650529 (Why is no real title available?)
• scientific article; zbMATH DE number 45228 (Why is no real title available?)
• A formulation of the simple theory of types
• Automating free logic in Isabelle/HOL
• Computational logic
• Cut-Simulation and Impredicativity
• Cut-elimination for quantified conditional logic
• Extending Sledgehammer with SMT solvers
• General models and extensionality
• Groups, Categories and Duality
• Higher-order semantics and extensionality
• Isabelle/HOL. A proof assistant for higher-order logic
• Logic for programming, artificial intelligence, and reasoning. 19th international conference, LPAR-19, Stellenbosch, South Africa, December 14--19, 2013. Proceedings
• More SPASS with Isabelle
• Nitpick: a counterexample generator for higher-order logic based on a relational model finder
• Satallax: An Automatic Higher-Order Prover
• The higher-order prover \textsc{Leo}-II

Cited in

(9)

• A comparison of HOL and ALF formalizations of a categorical coherence theorem
• Positive Free Higher-Order Logic and Its Automation via a Semantical Embedding
• Computer-supported exploration of a categorical axiomatization of modeloids
• Automating free logic in Isabelle/HOL
• Towards a readable formalisation of category theory
• Nuprl as logical framework for automating proofs in category theory
• A cut-free, sound and complete Russellian theory of definite descriptions
• Category theory in Isabelle/HOL as a basis for meta-logical investigation
• From Proof Nets to the Free *-Autonomous Category

Describes a project that uses

Uses Software

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

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

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2303232)