Abstract
In this paper, we propose a representative model based algorithm to calculate maximal contractions. For a formal theory Γ and a fact set Δ, the algorithm begins by accepting all models of refutation by facts of Γ with respect to Δ and filters these models to obtain the models of R-refutation. According to the completeness of R-calculus, the relevant maximal contraction is obtained simultaneously. In order to improve the efficiency, we divide the models into different classes according to the assignments of atomic propositions and only select relevant representative models to verify the satisfiability of each proposition. The algorithm is correct, and all maximal contractions of a given problem can be calculated by it. Users could make a selection according to their requirements. A benchmark algorithm is also provided. Experiments show that the algorithm has a good performance on normal revision problems.
Similar content being viewed by others
References
Li W. A logical framework for evolution of specifications. In: Proceedings of the 5th European Symposium on Programming. Edinburgh: Springer-Verlag Press, 1994. 394–408
Li W. Logical verification of scientific discovery. Sci China Inf Sci, 2010, 53: 677–684
Alchourron C, Gardenfors P, Makinson D. On The logic of theory change: partial meet contraction and revision functions. J Symbol Logic, 1985, 50: 510–530
Katsuno H, Mendelzon A O. A unified view of propositional knowledge base updates. In: Proceedings of the 11th International Joint Conference on Artificial Intelligence, Detroit, 1989. 1413–1419
Dalal M. Investigations into a theory of knowledge base revision: Preliminary report. In: Proceedings of the Seventh National Conference on Artificial Intelligence. Cambridge: AAAI Press, 1988. 475–479
Nebel B. Belief revision and default reasoning: Syntax-based approaches. In: Proceedings of the 2nd International Conference on Principles of Knowledge Representation and Reasoning, Cambridge, 1991. 417–428
Delgrande J P, Schaub T. A consistency-based model for belief change: Preliminary report. In: Proceedings of the AAAI National Conference on Artificial Intelligence, Austin, 2000. 392–398
Li W. A development calculus for specifications. Sci China Ser F-Inf Sci, 2003, 46: 390–400
Li W. R-calculus: an inference system for belief revision. Comput J, 2007, 50: 378–390
Jiang D C, Lou Y H, Jin Y. A revision approach based on assignment equivalence classes. In: Proceedings of 2nd International Workshop on Intelligent Systems and Applications, Wuhan, 2010. 1199–1202
Luo J, Li W. An algorithm to computer maximal contractions for Horn clauses. Sci China Inf Sci, 2011, 55: 244–257
Li W. Mathematical Logic-Foundations for Information Science. Basel: Birkhäauser Verlag, 2010
Author information
Authors and Affiliations
Corresponding author
Rights and permissions
About this article
Cite this article
Jiang, D., Lou, Y., Jin, Y. et al. A representative model based algorithm for maximal contractions. Sci. China Inf. Sci. 56, 1–13 (2013). https://doi.org/10.1007/s11432-012-4752-y
Received:
Accepted:
Published:
Issue Date:
DOI: https://doi.org/10.1007/s11432-012-4752-y