Recommendations
Cites work
- scientific article; zbMATH DE number 3904558 (Why is no real title available?)
- scientific article; zbMATH DE number 4094866 (Why is no real title available?)
- scientific article; zbMATH DE number 1189096 (Why is no real title available?)
- scientific article; zbMATH DE number 1189106 (Why is no real title available?)
- scientific article; zbMATH DE number 1341619 (Why is no real title available?)
- scientific article; zbMATH DE number 1950261 (Why is no real title available?)
- scientific article; zbMATH DE number 1950272 (Why is no real title available?)
- scientific article; zbMATH DE number 1552522 (Why is no real title available?)
- scientific article; zbMATH DE number 1552523 (Why is no real title available?)
- scientific article; zbMATH DE number 1552529 (Why is no real title available?)
- scientific article; zbMATH DE number 1552532 (Why is no real title available?)
- scientific article; zbMATH DE number 1765683 (Why is no real title available?)
- scientific article; zbMATH DE number 194631 (Why is no real title available?)
- scientific article; zbMATH DE number 2090306 (Why is no real title available?)
- scientific article; zbMATH DE number 837700 (Why is no real title available?)
- scientific article; zbMATH DE number 3274715 (Why is no real title available?)
- scientific article; zbMATH DE number 3407195 (Why is no real title available?)
- A Computing Procedure for Quantification Theory
- A Machine-Oriented Logic Based on the Resolution Principle
- A machine program for theorem-proving
- A nucleus of a theorem-prover described inAlgol-68
- An improved proof procedure1
- Automated Deduction – CADE-20
- Automated Reasoning
- Basic narrowing revisited
- Controlled integration of the cut rule into connection tableau calculi
- Depth-first proof search without backtracking for free-variable clausal tableaux
- Eliminating dublication with the hyper-linking strategy
- On Matrices with Connections
- Ordered semantic hyper-linking
- Paramodulation-based theorem proving
- Partial instantiation methods for inference in first-order logic
- Proof and model generation with disconnection tableaux
- Proving Theorems with the Modification Method
- Refutation graphs
- Rewrite-based Equational Theorem Proving with Selection and Simplification
- Rewriting
- Simplification rules for constrained formula tableaux
- Term Rewriting and All That
- The model evolution calculus.
- Theorem Proving via General Matings
- lean\(T^ AP\): Lean tableau-based deduction
Cited in
(13)- Automated Reasoning
- scientific article; zbMATH DE number 1612557 (Why is no real title available?)
- Proof and model generation with disconnection tableaux
- Automated Reasoning with Analytic Tableaux and Related Methods
- Connection tableau calculi with disjunctive contraints (TU München)
- Certification of nonclausal connection tableaux proofs
- The disconnection method
- Connection Tableaux with Lazy Paramodulation
- Connection tableau calculi with disjunctive constraints
- scientific article; zbMATH DE number 1950272 (Why is no real title available?)
- scientific article; zbMATH DE number 1765683 (Why is no real title available?)
- Universal variables in disconnection tableaux
- Connection tableaux with lazy paramodulation
This page was built for publication: The disconnection tableau calculus
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q877889)
