scientific article; zbMATH DE number 1552524
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].
- Set of support, demodulation, paramodulation: a historical perspective
- Towards a unified model of search in theorem-proving: subgoal-reduction strategies
- Model elimination and connection tableau procedures
- Semantically-guided goal-sensitive reasoning: model representation
- Introducing general redundancy criteria for clausal tableaux, and proposing resolution tableaux
- Restart tableaux with selection function
- scientific article; zbMATH DE number 1552523 (Why is no real title available?)
- scientific article; zbMATH DE number 1748583 (Why is no real title available?)
- scientific article; zbMATH DE number 1841823 (Why is no real title available?)
- scientific article; zbMATH DE number 834568 (Why is no real title available?)
- Hyper tableaux
This page was built for publication:
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q4524784)
