Automating free logic in HOL, with an experimental application in category theory
From MaRDI portal
Publication:2303232
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
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
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
