Checking several forms of consistency in nonmonotonic knowledge-bases

  • Bertrand Mazure
  • Lakhdar Saïs
  • Éric Grégoire
Invited Papers
Part of the Lecture Notes in Computer Science book series (LNCS, volume 1244)


In this paper, a new method is introduced to check several forms of logical consistency in nonmonotonic knowledge-bases (KBs). The knowledge representation language under consideration is full propositional logic, using “Abnormal” propositions to be minimized. Basically, the method is based on the use of local search techniques for SAT. Since these techniques are by nature logically incomplete, it is often believed that they can only show that a formula is consistent. Surprisingly enough, we find that they can allow inconsistency to be proved as well. To that end, some additional heuristic information about the work performed by local search algorithms is shown of prime practical importance. Adapting this heuristic and using some specific minimization policies, we propose some possible strategies to exhibit a “normal-circumstances” model or simply a model of the KB, or to show their non-existence.


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. 1.
    Davis, M., Putnam, H.: A Computing Procedure for Quantification Theory. Journ. of the ACM 7 (1960) 201–215Google Scholar
  2. 2.
    Proc. of the Second DIMACS Challenge on Satisfiability Testing, Rutgers (1993)Google Scholar
  3. 3.
    Dubois, O., André, P., Boufkhad, Y., Carlier, J.: SAT vs. UNSAT, in [2].Google Scholar
  4. 4.
    Jeroslow, R.E., Wang, J.: Solving Propositional Satisfiability Problems. Ann. Maths and AI 1 (1990) 167–187Google Scholar
  5. 5.
    azure, B., Saïs, L., Grégoire, E.: TWSAT: a New Local Search Algorithm for SAT. Performance and Analysis. CP'95 Workshop on Studying and Solving Really Hard Problems, Cassis, France (1995) 127–130 (full version in Proc. AAAI-97)Google Scholar
  6. 6.
    azure, B., Saïs, L., Grégoire, E.: Detecting logical inconsistencies. Proc. AI and Maths Symposium, Fort Lauderdale (FL) (1196) 116–121Google Scholar
  7. 7.
    McCarthy, J.: Applications of circumscription for formalizing common-sense knowledge. Artificial Intelligence 28 (1986) 89–116Google Scholar
  8. 8.
    Mitchell, D., Selman, B., Levesque, H.: Hard and Easy Distributions of SAT Problems. Proc. AAAI-92 (1992) 459–465Google Scholar
  9. 9.
    Reiter, R.: A theory of diagnosis from first principles. Artificial Intelligence 32 (1987) 57–95Google Scholar
  10. 10.
    Reiter, R.: A logic for default reasoning. Artificial Intelligence 13 (1980) 81–131Google Scholar
  11. 11.
    Selman, B., Levesque, H., Mitchell, D.: A New Method for Solving Hard Satisfiability Problems. Proc. AAAI-92 (1992) 440–446Google Scholar
  12. 12.
    Selman, B., Kautz, H.A., Cohen, B.: Local Search Strategies for Satisfiability Testing. Proc. DIMACS Workshop on Maximum Clique, Graph Coloring, and Satisfiability (1993)Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 1997

Authors and Affiliations

  • Bertrand Mazure
    • 1
  • Lakhdar Saïs
    • 1
  • Éric Grégoire
    • 1
  1. 1.CRIL - Université d'ArtoisLens CedexFrance

Personalised recommendations