A sound framework for -rule variants in free-variable semantic tableaux

DOI10.1007/S10817-006-9045-YMaRDI QIDQ877883zbMATH OpenOpenAlexFDO

Authors Marianna Nicolosi Asmundo, Domenico Cantone

Publication date 4 May 2007

Published in Journal of Automated Reasoning (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/s10817-006-9045-y

zbMATH Keywords

Skolemizationdelta-rule

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35)

Recommendations

• scientific article; zbMATH DE number 1507185
• The liberalized -rule in free variable semantic tableaux
• scientific article; zbMATH DE number 517067
• Tableau methods for a logic with term declarations
• Simplification rules for constrained formula tableaux

Cites work

• scientific article; zbMATH DE number 1341475 (Why is no real title available?)
• scientific article; zbMATH DE number 517067 (Why is no real title available?)
• scientific article; zbMATH DE number 1142316 (Why is no real title available?)
• scientific article; zbMATH DE number 1950267 (Why is no real title available?)
• scientific article; zbMATH DE number 1507185 (Why is no real title available?)
• scientific article; zbMATH DE number 1552511 (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?)
• A Free Variable Version of the First-Order Predicate Calculus
• A sound framework for \(\delta\)-rule variants in free-variable semantic tableaux
• First-order tableau methods
• Model elimination and connection tableau procedures
• Tableaux and related methods
• The liberalized -rule in free variable semantic tableaux

Cited in

(6)

• scientific article; zbMATH DE number 517067 (Why is no real title available?)
• scientific article; zbMATH DE number 1507185 (Why is no real title available?)
• \(\lim +, \delta^+\), and non-permutability of \(\beta\)-steps
• A sound framework for \(\delta\)-rule variants in free-variable semantic tableaux
• Efficient elimination of Skolem functions in \(\text{LK}^\text{h} \)
• The liberalized -rule in free variable semantic tableaux

Describes a project that uses

Uses Software

• GQML
• TABLEAUX
• GULP

This page was built for publication: A sound framework for \(\delta\)-rule variants in free-variable semantic tableaux

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