Proof and model generation with disconnection tableaux

DOI10.1007/3-540-45653-8_10MaRDI QIDQ2996159zbMATH OpenOpenAlexFDO

Authors Reinhold Letz, Gernot Stenz

Publication date 6 May 2011

Published in Logic for Programming, Artificial Intelligence, and Reasoning (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/3-540-45653-8_10

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35)

Recommendations

• The disconnection tableau calculus
• Automated Reasoning
• scientific article; zbMATH DE number 1765683
• Universal variables in disconnection tableaux
• scientific article; zbMATH DE number 1950261

Cited in

(14)

• Automated Reasoning with Analytic Tableaux and Related Methods
• First order Stålmarck. Universal lemmas through branch merges
• Semantically-guided goal-sensitive reasoning: inference system and completeness
• Semantically-guided goal-sensitive reasoning: model representation
• scientific article; zbMATH DE number 1552524 (Why is no real title available?)
• Computing finite models by reduction to function-free clause logic
• Comparing instance generation methods for automated reasoning
• A Tableaux Method for Systematic Simultaneous Search for Refutations and Models using Equational Problems
• The disconnection tableau calculus
• scientific article; zbMATH DE number 1765683 (Why is no real title available?)
• Universal variables in disconnection tableaux
• Fully reusing clause deduction algorithm based on standard contradiction separation rule
• The model evolution calculus as a first-order DPLL method
• Automated Reasoning

Describes a project that uses

Uses Software

• DCTP
• FINDER

This page was built for publication: Proof and model generation with disconnection tableaux

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2996159)