Proof and model generation with disconnection tableaux

DOI10.1007/3-540-45653-8_10zbMATH Open1275.03081OpenAlexW55835010MaRDI QIDQ2996159FDOQ2996159

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

Recommendations

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

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35)

Cited In (14)

• Automated Reasoning with Analytic Tableaux and Related Methods
• First order Stålmarck. Universal lemmas through branch merges
• Title not available (Why is that?)
• Semantically-guided goal-sensitive reasoning: inference system and completeness
• Semantically-guided goal-sensitive reasoning: model representation
• A Tableaux Method for Systematic Simultaneous Search for Refutations and Models using Equational Problems
• Computing finite models by reduction to function-free clause logic
• Comparing instance generation methods for automated reasoning
• The disconnection tableau calculus
• Title not available (Why is that?)
• 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

Uses Software

• FINDER
• DCTP

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)