Nothing Special   »   [go: up one dir, main page]
Skip to main content
Springer Nature Link
Log in

A decomposition based algorithm for maximal contractions

  • Research Article
  • Published:
Frontiers of Computer Science Aims and scope Submit manuscript

Abstract

This paper proposes a decomposition based algorithm for revision problems in classical propositional logic. A set of decomposing rules are presented to analyze the satisfiability of formulas. The satisfiability of a formula is equivalent to the satisfiability of a set of literal sets. A decomposing function is constructed to calculate all satisfiable literal sets of a given formula. When expressing the satisfiability of a formula, these literal sets are equivalent to all satisfied models of such formula. A revision algorithm based on this decomposing function is proposed, which can calculate maximal contractions of a given problem. In order to reduce the memory requirement, a filter function is introduced. The improved algorithm has a good performance in both time and space perspectives.

This is a preview of subscription content, log in via an institution to check access.

Access this article

Log in via an institution

Subscribe and save

Springer+ Basic
$34.99 /Month
  • Get 10 units per month
  • Download Article/Chapter or eBook
  • 1 Unit = 1 Article or 1 Chapter
  • Cancel anytime
Subscribe now

Buy Now

Price excludes VAT (USA)
Tax calculation will be finalised during checkout.

Instant access to the full article PDF.

Institutional subscriptions

Similar content being viewed by others

References

  1. Li W. A logical framework for evolution of specifications. In: Proceedings of the 5th European Symposium on Programming. 1994, 4: 394–408

    Google Scholar 

  2. Li W. Logical verification of scientific discovery. Science China Information Sciences, 2010, 53(4): 677–884

    Article  MathSciNet  Google Scholar 

  3. Jiang D, Lou Y, Jin Y, Luo J, Li W. A representative model based algorithm for maximal contractions. Science China Information Sciences, 2013, 56(1): 1–13

    MathSciNet  Google Scholar 

  4. Alchourrón C, Gärdenfors P, Makinson D. On the logic of theory change: partial meet contraction and revision functions. Journal of Symbolic Logic, 1985, 50(2): 510–530

    Article  MathSciNet  MATH  Google Scholar 

  5. Katsuno H, Mendelzon A O. A unified view of propositional knowledge base updates. In: Proceedings of the 11th International Joint Conference on Artificial Intelligence. 1989, 1413–1419

    Google Scholar 

  6. Darwiche A, Pearl J. On the logic of iterated belief revision[j]. Artificial Intelligence, 1997, 89: 1–29

    Article  MathSciNet  MATH  Google Scholar 

  7. Dalal M. Investigations into a theory of knowledge base revision: preliminary report[c]. In: Proceedings of the 7th National Conference on Artificial Intelligence. 1988, 8: 475–479

    Google Scholar 

  8. Nebel B. Belief revision and default reasoning: Syntax-based approaches. In: Proceedings of the 2nd International Conference on Principles of Knowledge Representation and Reasoning. 1991, 4: 417–428

    MathSciNet  Google Scholar 

  9. Delgrande J P, Schaub T. A consistency-based approach for belief change. Artificial Intelligence, 2003, 151(1): 1–41

    Article  MathSciNet  MATH  Google Scholar 

  10. Li W. A development calculus for specifications. Science in China Series F: Information Sciences, 2003, 46(5): 390–400

    Article  MathSciNet  MATH  Google Scholar 

  11. Li W. R-calculus: An inference system for belief revision. The Computer Journal, 2007, 50(4): 378–390

    Article  Google Scholar 

  12. Luo J, Li W. An algorithm to compute maximal contractions for horn clauses. Science China Information Sciences, 2011, 54(2): 244–257

    Article  MathSciNet  MATH  Google Scholar 

  13. Luo J. A general framework for computing maximal contractions. Frontiers of Computer Science, 2013, 7(1): 83–94

    Article  Google Scholar 

  14. Luo J, Li W. R-calculus without the cut rule. Science China Information Sciences, 2011, 54(12): 1–14

    Article  MathSciNet  Google Scholar 

Download references

Author information

Authors and Affiliations

  1. State Key Laboratory of Computer Architecture, Institute of Computing Technology, Chinese Academy of Sciences, Beijing, 100190, China

    Dongchen Jiang

  2. State Key Laboratory of Software Development Environment, Beihang University, Beijing, 100191, China

    Dongchen Jiang, Wei Li, Jie Luo & Yihua Lou

  3. Tencent Technology (Beijing) Company Limited, Beijing, 100080, China

    Zhengzhong Liao

Authors
  1. Dongchen Jiang
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Wei Li
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Jie Luo
    View author publications

    You can also search for this author in PubMed Google Scholar

  4. Yihua Lou
    View author publications

    You can also search for this author in PubMed Google Scholar

  5. Zhengzhong Liao
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Dongchen Jiang.

Additional information

Dongchen Jiang received his PhD degree in computer science from Beihang University, China, in 2013. He is an assistant professor in the Institute of Computer Technology of the Chinese Academy of Sciences. His research interests include automated reasoning, formal verification, automatic and interactive theorem proving, and program verification.

Wei Li is a professor of the school of computer science and engineering, Beihang University, China, and he is an academician of the Chinese Academy of Sciences.

Jie Luo is a lecturer of the School of Computer Science and Engineering, Beihang University, Beijing, China. His research interests include mathematical logic, formal method, automated reasoning, and software debugging.

Yihua Lou received his BS from the Beihang University in 2006, and is now a PhD candidate in State Key Laboratory of Software Development Environment, Beihang University. His research interests include human-computer interaction, multimedia, and cloud computing.

Zhengzhong Liao is an experienced researcher, who has worked on the research and development of internet maps and street view for more than three years in Tencent Beijing Ltd. He got his MS from Beihang University. He is highly skilled in software design and development, and recently his effort is mainly on mobile internet technology and products, besides some computer science theories.

Rights and permissions

Reprints and permissions

About this article

Cite this article

Jiang, D., Li, W., Luo, J. et al. A decomposition based algorithm for maximal contractions. Front. Comput. Sci. 7, 801–811 (2013). https://doi.org/10.1007/s11704-013-3089-z

Download citation

  • Received:

  • Accepted:

  • Published:

  • Issue Date:

  • DOI: https://doi.org/10.1007/s11704-013-3089-z

Keywords

Search

Navigation