Incremental theory reasoning methods for semantic tableaux
From MaRDI portal
Publication:4645229
DOI10.1007/3-540-61208-4_7zbMATH Open1412.68208OpenAlexW1482455082MaRDI QIDQ4645229FDOQ4645229
Authors: Bernhard Beckert, Christian Pape 
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
Recommendations
Cites Work
- Title not available (Why is that?)
- Title not available (Why is that?)
- Automated deduction by theory resolution
- A Simplified Format for the Model Elimination Theorem-Proving Procedure
- Title not available (Why is that?)
- The liberalized \(\delta\)-rule in free variable semantic tableaux
- Title not available (Why is that?)
- Title not available (Why is that?)
- Basic narrowing revisited
- Theorem proving using equational matings and rigid E -unification
- A completion-based method for mixed universal and rigid \(E\)-unification
- The undecidability of simultaneous rigid E-unification
- Seventy-five problems for testing automatic theorem provers
- Linear and unit-resulting refutations for Horn theories
- Title not available (Why is that?)
- Title not available (Why is that?)
Cited In (9)
- Deduction by combining semantic tableaux and integer programming
- Adding equality to semantic tableaux
- The tableau-based theorem prover 3 T A P Version 4.0
- First-order automated reasoning with theories: when deduction modulo theory meets practice
- Bottom-up Construction of Semantic Tableaux
- Semantic tableaux with equality
- Title not available (Why is that?)
- Title not available (Why is that?)
- Incremental Tabling in Support of Knowledge Representation and Reasoning
Uses Software
This page was built for publication: Incremental theory reasoning methods for semantic tableaux
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q4645229)
