Abstract
"Hyper tableau" is a sound and complete calculus for first- order clausal logic. The present paper introduces an improvement which removes the major weakness of the calculus, which is the need to (at least partially) blindly guess ground-instantiations for certain clauses. This guessing is now replaced by a unification-driven technique. The calculus is presented in detail, which includes a completeness proof. Completeness is proven by using a novel approach to extract a model from an open branch. This enables semantical redundancy criteria which are not present in related approaches. Supported by the DFG within the research programme "Deduction" under grant Fu 263-2. © Springer-Verlag Berlin Heidelberg 1998.
Cite
CITATION STYLE
Baumgartner, P. (1998). Hyper tableau - The next generation. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 1397 LNAI, pp. 60–76). Springer Verlag. https://doi.org/10.1007/3-540-69778-0_14
Register to see more suggestions
Mendeley helps you to discover research relevant for your work.
