Automating free logic in Isabelle/HOL

DOI10.1007/978-3-319-42432-3_6MaRDI QIDQ2819197zbMATH OpenOpenAlexFDO

Authors Christoph Benzmüller, Dana 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

application to category theoryfree logicinteractive and automated theorem provingmodel finding

Mathematics Subject Classification ID

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

Recommendations

• Automating free logic in HOL, with an experimental application in category theory
• Positive Free Higher-Order Logic and Its Automation via a Semantical Embedding
• The Isabelle Framework
• Automatic proof and disproof in Isabelle/HOL
• The foundation of a generic theorem prover

Cites work

• \textsc{LeoPARD} -- a generic platform for the implementation of higher-order reasoners
• Extending Sledgehammer with SMT solvers
• scientific article; zbMATH DE number 5850137 (Why is no real title available?)
• scientific article; zbMATH DE number 45228 (Why is no real title available?)
• Isabelle/HOL. A proof assistant for higher-order logic

Cited in

(14)

• Automating free logic in HOL, with an experimental application in category theory
• Extensional higher-order paramodulation in Leo-III
• Nonfree datatypes in Isabelle/HOL. Animating a many-sorted metatheory
• Foundational, compositional (co)datatypes for higher-order logic: category theory applied to theorem proving
• Automated Engineering of Relational and Algebraic Methods in Isabelle/HOL
• scientific article; zbMATH DE number 1867306 (Why is no real title available?)
• Logic-Free Reasoning in Isabelle/Isar
• I/O logic in HOL
• Category theory in Isabelle/HOL as a basis for meta-logical investigation
• Positive Free Higher-Order Logic and Its Automation via a Semantical Embedding
• Dyadic deontic logic in HOL: faithful embedding and meta-theoretical experiments
• Gödel's God in Isabelle/HOL
• Exploring Simplified Variants of Gödel’s Ontological Argument in Isabelle/HOL
• Anselm's God in Isabelle/HOL

Describes a project that uses

Uses Software

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

This page was built for publication: Automating free logic in Isabelle/HOL

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