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

DOI10.1007/S10817-018-09507-7zbMATH Open1434.68639OpenAlexW2908410917MaRDI QIDQ2303232FDOQ2303232

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

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

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)

Cites Work

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

Cited In (5)

• Computer-Supported Exploration of a Categorical Axiomatization of Modeloids
• Positive Free Higher-Order Logic and Its Automation via a Semantical Embedding
• 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

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

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)