A framework for using knowledge in tableau proofs
From MaRDI portal
Publication:4610337
DOI10.1007/BFb0027424zbMath1412.68262OpenAlexW1596013579MaRDI QIDQ4610337
Publication date: 15 January 2019
Published in: Lecture Notes in Computer Science (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1007/bfb0027424
Uses Software
Cites Work
- Manifolds, tensor analysis, and applications.
- SETHEO: A high-performance theorem prover
- Gazing: An approach to the problem of definition and lemma use
- Towards the automation of set theory and its logic
- Controlled integration of the cut rule into connection tableau calculi
- The liberalized \(\delta\)-rule in free variable semantic tableaux
- A-ordered tableaux
- A Beginner's Further Guide to Mathematical Logic
- Fast Decision Procedures Based on Congruence Closure
- An algorithm for reasoning about equality
- A completion-based method for mixed universal and rigid E-unification
- Hyper tableaux
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item