A sound framework for \(\delta\)-rule variants in free-variable semantic tableaux

DOI10.1007/s10817-006-9045-yzbMath1121.03020OpenAlexW1985365096MaRDI QIDQ877883

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)

Related Items

Efficient elimination of Skolem functions in \(\text{LK}^\text{h} \) ⋮ A sound framework for \(\delta\)-rule variants in free-variable semantic tableaux ⋮ \(\lim +, \delta^+\), and non-permutability of \(\beta\)-steps

Uses Software

• GULP
• TABLEAUX
• GQML

Cites Work

• A sound framework for \(\delta\)-rule variants in free-variable semantic tableaux
• The liberalized \(\delta\)-rule in free variable semantic tableaux
• A Free Variable Version of the First-Order Predicate Calculus
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item