Incremental theory reasoning methods for semantic tableaux
From MaRDI portal
Publication:4645229
DOI10.1007/3-540-61208-4_7zbMath1412.68208OpenAlexW1482455082MaRDI QIDQ4645229
Christian Pape, Bernhard Beckert
Publication date: 10 January 2019
Published in: Theorem Proving with Analytic Tableaux and Related Methods (Search for Journal in Brave)
Full work available at URL: https://publikationen.bibliothek.kit.edu/21696/1953
Lua error in Module:PublicationMSCList at line 37: attempt to index local 'msc_result' (a nil value).
Related Items (2)
First-order automated reasoning with theories: when deduction modulo theory meets practice ⋮ The tableau-based theorem prover 3 T A P Version 4.0
Uses Software
Cites Work
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- The undecidability of simultaneous rigid E-unification
- Seventy-five problems for testing automatic theorem provers
- The liberalized \(\delta\)-rule in free variable semantic tableaux
- Automated deduction by theory resolution
- Basic narrowing revisited
- Linear and unit-resulting refutations for Horn theories
- Theorem proving using equational matings and rigid E -unification
- A completion-based method for mixed universal and rigid E-unification
- A Simplified Format for the Model Elimination Theorem-Proving Procedure
This page was built for publication: Incremental theory reasoning methods for semantic tableaux
