Welcome!
To use the personalized features of this site, please log in or register.
If you have forgotten your username or password, we can help.
My Menu
Saved Items

Constrained Hyper Tableaux

Jan van Eijck5, 6 Contact Information

(5)  Uil-OTS, Utrecht
(6)  CWI and ILLC, Amsterdam
Abstract
Hyper tableau reasoning is a version of clausal form tableau reasoning where all negative literals in a clause are resolved away in a single inference step. Constrained hyper tableaux are a generalization of hyper tableaux, where branch closing substitutions, from the point of view of model generation, give rise to constraints on satisfying assignments for the branch. These variable constraints eliminate the need for the awkward ‘purifying substitutions’ of hyper tableaux. The paper presents a non-destructive and proof confluent calculus for constrained hyper tableaux, together with a soundness and completeness proof, with completeness based on a new way to generate models from open tableaux. It is pointed out that the variable constraint approach applies to free variable tableau reasoning in general.

Contact Information Jan van Eijck
Email: jve@cwi.nl
Fulltext Preview (Small, Large)
Image of the first page of the fulltext

References secured to subscribers.



Export this chapter
Export this chapter as RIS | Text
 
Remote Address: 38.107.191.107 • Server: mpweb16
HTTP User Agent: CCBot/1.0 (+http://www.commoncrawl.org/bot.html)