No label defined (Q4524784)

Further refinements regarding connection tableaux and model elimination are introduced; this is understood to incorporate goal directedness into tableau calculi. In this paper concentration is on two aspects: Firstly, the model elimination variant of connection tableaux is refined. This results in a new calculus which is called Restart Model Elimination (RME). RME is motivated by its much more natural reading of clauses than in model elimination, but at the same time keeping its goal orientedness. Secondly a different direction is pursued, namely defining clausal tableaux in a purely bottom up way. This direction was motivated by the success of model generating procedures like SATCHMO and the MGTP system. For the first aspect variants of RME are introduced and its properties are discussed. For the second aspect on forward chaining an extension to the SATCHMO-like approaches is introduced. This calculus is called ``hyper tableau'' and allows to treat variables more efficiently than related approaches. For the entire collection see [Zbl 0948.00015].