An algorithm to compute maximal contractions for Horn clauses. (English) Zbl 1229.03015
In this paper the authors address the problem of computing maximal subsets of a set \(\Gamma\) of formulae which are consistent with a set \(\Delta\) of facts (i.e. maximal contractions). For this, the authors proceed as follows:
- (1)
- They prove a conversion relationship between minimal inconsistent sets of the union of \(\Gamma\) and \(\Delta\) and maximal contractions.
- (2)
- They give a necessary condition of a set of Horn clauses to be minimal inconsistent.
- (3)
- Based on these two results, they give an algorithm for enumerating all minimal inconsistent subsets of a given set of Horn clauses, and an algorithm for computing the maximal contractions from these minimal inconsistent subsets.
- (4)
- They propose an (interactive) algorithm for computing maximal contractions for Horn clauses by composing the above algorithms.
MSC:
| 03B35 | Mechanization of proofs and logical operations |
| 03B42 | Logics of knowledge and belief (including belief change) |
| 68T15 | Theorem proving (deduction, resolution, etc.) (MSC2010) |
Keywords:
Horn clause; minimal inconsistent set; maximal contraction; minimal subtraction; belief revisionReferences:
| [1] | Li W. A logical framework for evolution of specifications. In: programming languages and systems–ESOP’94. LNCS 788, Berlin: Springer-Verlag, 1994. 394–408 |
| [2] | Li W. R-calculus: an inference system for belief revision. Comput J, 2007, 50: 378–390 · doi:10.1093/comjnl/bxl069 |
| [3] | Li W. Mathematical Logic – Foundations For Information Science. Basel: Birkhäuser Verlag, 2010 · Zbl 1185.03001 |
| [4] | Gallier J H. Logic for Computer Science: Foundations of Automatic Theorem Proving. New York: Harper & Row, 1986 · Zbl 0605.03004 |
| [5] | Delgrande J P. Horn Clause Belief Change: Contraction Functions. In: Proc KR 2008. Menlo Park: AAAI Press, 2008. 156–165 |
| [6] | Booth R, Meyer T, Varzinczak I J. Next steps in propositional Horn contraction. In: Proc IJCAI 2009. Menlo Park: AAAI Press, 2009. 702–707 |
| [7] | Alchourrón C E, Gärdenfors R, Makinson D. On the logic of theory change: partial meet contraction and revision functions. J Symbolic Logic, 1985, 50: 510–530 · Zbl 0578.03011 · doi:10.2307/2274239 |
| [8] | Gärdenfors P. Knowledge in Flux. Modeling the Dynamics of Epistemic States. Cambridge: The MIT Press, 1988 · Zbl 1229.03008 |
| [9] | Gärdenfors P, Makinson D. Revisions of Knowledge Systems Using Epistemic Entrenchment. In: Second Conference on Theoretical Aspects of Reasoning about Knowledge, San Francisco: Morgan Kaufmann Publishers Inc., 1988. 83–95 · Zbl 0711.03009 |
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.
