Incremental theory reasoning methods for semantic tableaux

DOI10.1007/3-540-61208-4_7MaRDI QIDQ4645229zbMATH OpenOpenAlexFDO

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

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35)

Recommendations

• scientific article; zbMATH DE number 1765699
• Theory reasoning in connection calculi
• scientific article; zbMATH DE number 1552522
• scientific article; zbMATH DE number 1552527
• Semantic tableaux with equality

Cites work

• scientific article; zbMATH DE number 46359 (Why is no real title available?)
• scientific article; zbMATH DE number 64168 (Why is no real title available?)
• scientific article; zbMATH DE number 1330425 (Why is no real title available?)
• scientific article; zbMATH DE number 517067 (Why is no real title available?)
• scientific article; zbMATH DE number 194631 (Why is no real title available?)
• scientific article; zbMATH DE number 3274715 (Why is no real title available?)
• scientific article; zbMATH DE number 3299786 (Why is no real title available?)
• A Simplified Format for the Model Elimination Theorem-Proving Procedure
• A completion-based method for mixed universal and rigid \(E\)-unification
• Automated deduction by theory resolution
• Basic narrowing revisited
• Linear and unit-resulting refutations for Horn theories
• Seventy-five problems for testing automatic theorem provers
• The liberalized -rule in free variable semantic tableaux
• The undecidability of simultaneous rigid E-unification
• Theorem proving using equational matings and rigid E -unification

Cited in

(9)

• Adding equality to semantic tableaux
• Deduction by combining semantic tableaux and integer programming
• The tableau-based theorem prover 3 T A P Version 4.0
• First-order automated reasoning with theories: when deduction modulo theory meets practice
• Semantic tableaux with equality
• Bottom-up Construction of Semantic Tableaux
• scientific article; zbMATH DE number 1765699 (Why is no real title available?)
• scientific article; zbMATH DE number 5511125 (Why is no real title available?)
• Incremental Tabling in Support of Knowledge Representation and Reasoning

Describes a project that uses

Uses Software

• 3TAP

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)