ML Anthology

A Theorem-Prover for a Decidable Subset of Default Logic

Philippe Besnard, Rene Quiniou, Patrice Quinton
AAAI 1983 pp. 27-30
/aaai/1983/besnard1983aaai-theorem/

Abstract

Non-monotonic logic is an attempt to take into account such notions as incomplete knowledge and theory evolution. However the decidable theorem-prover issue has been so far unexplored. We propose such a theorem-prover for default logic with a restriction on the first-order formulae it deals with. This theorem-prover is based on the generalisation of a resolution technique named saturation, which was initially designed to test the consistency of a set of first-order formulae. We have proved that our algorithm is complete and that it always terminates for the selected subset of first-order formulae.

PDF AAAI Semantic Scholar

Cite

Text

Besnard et al. "A Theorem-Prover for a Decidable Subset of Default Logic." AAAI Conference on Artificial Intelligence, 1983.

Markdown

[Besnard et al. "A Theorem-Prover for a Decidable Subset of Default Logic." AAAI Conference on Artificial Intelligence, 1983.](https://mlanthology.org/aaai/1983/besnard1983aaai-theorem/)

BibTeX

@inproceedings{besnard1983aaai-theorem,
  title     = {{A Theorem-Prover for a Decidable Subset of Default Logic}},
  author    = {Besnard, Philippe and Quiniou, Rene and Quinton, Patrice},
  booktitle = {AAAI Conference on Artificial Intelligence},
  year      = {1983},
  pages     = {27-30},
  url       = {https://mlanthology.org/aaai/1983/besnard1983aaai-theorem/}
}