Invited Talk: On a (Quite) Universal Theorem Proving Approach and Its Application in Metaphysics
From MaRDI portal
Publication:3455772
DOI10.1007/978-3-319-24312-2_15zbMath1471.68302OpenAlexW1927497685MaRDI QIDQ3455772
Publication date: 11 December 2015
Published in: Lecture Notes in Computer Science (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1007/978-3-319-24312-2_15
Philosophical and critical aspects of logic and foundations (03A05) Mechanization of proofs and logical operations (03B35) Higher-order logic (03B16) Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15)
Related Items (1)
Uses Software
Cites Work
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- The higher-order prover \textsc{Leo}-II
- Computer-assisted analysis of the Anderson-Hájek ontological controversy
- Combining and automating classical and non-classical logics in classical higher-order logics
- Computer supported mathematics with \(\Omega\)MEGA
- Embedding and automating conditional logics in classical higher-order logic
- Quantified multimodal logics in simple type theory
- Extending Sledgehammer with SMT solvers
- Proof planning with multiple strategies
- The TPTP problem library and associated infrastructure and associated infrastructure. The FOF and CNF parts, v3.5.0
- On Logic Embeddings and Gödel’s God
- HOL Based First-Order Modal Logic Provers
- Satallax: An Automatic Higher-Order Prover
- Higher-Order Modal Logics: Automation and Applications
- Multimodal and intuitionistic logics in simple type theory
- Interacting with Modal Logics in the Coq Proof Assistant
- Semantics-Based Translation Methods for Modal Logics
- Functional translation and second-order frame properties of modal logics
- Nitpick: A Counterexample Generator for Higher-Order Logic Based on a Relational Model Finder
This page was built for publication: Invited Talk: On a (Quite) Universal Theorem Proving Approach and Its Application in Metaphysics
