Linear and unit-resulting refutations for Horn theories (Q1923821): Difference between revisions
From MaRDI portal
Removed claim: reviewed by (P1447): Item:Q583186 |
Changed an Item |
||
Property / reviewed by | |||
Property / reviewed by: N. K. Zamov / rank | |||
Normal rank |
Revision as of 08:35, 16 February 2024
scientific article
Language | Label | Description | Also known as |
---|---|---|---|
English | Linear and unit-resulting refutations for Horn theories |
scientific article |
Statements
Linear and unit-resulting refutations for Horn theories (English)
0 references
21 April 1997
0 references
The paper presents an approach to combine two effective resolution strategies for a Horn clause set. The proposed method consists of saturating a Horn clause set under several deduction operations by adding new inference rules until only redundant consequences can be added. This technique -- called linearizing completion -- allows to combine the unit-resulting resolution strategy with a linear strategy à la Prolog in a refutationally complete way. This is not trivial, since although each strategy alone is complete for Horn theories, their naive combination is not. A redundancy criterion allows deletion of many of added inference rules, which makes the resulting inference systems quite compact. The transformed theory can be used in combination with linear calculi, such as, e.g., model elimination, to yield sound, complete and efficient calculi for full first-order clause logic over the given Horn theory. The method has been implemented and has been tested in conjunction with a model-elimination theorem prover.
0 references
unit resolution
0 references
Horn clause
0 references
linear strategy
0 references
redundancy criterion
0 references
first-order clause logic
0 references
Horn theory
0 references
model-elimination
0 references