Non-Clausal Reasoning with Definite Theories

• Autorzy: Stachniak Z.
• Języki publikacji: EN

Abstrakty

EN

In this paper we propose a general-purpose first-order automated reasoning framework based on the notion of a definite formula and on a non-clausal variant of SLD-resolution. This framework provides a universal Horn clause-like representation of knowledge for classical as well as a range of non-classical first-order logics. It provides a resolution-style method for automated reasoning with theories of definite formulas.

Słowa kluczowe

EN

automated reasoning; non-clausal resolution; definite formula

• Wydawca: IOS Press
• Czasopismo: Fundamenta Informaticae
• Rocznik: 2001
• Tom: Vol. 48, nr 4
• Strony: 363--388
• Opis fizyczny: bibliogr. 22 poz.

Twórcy

autor

Stachniak Z.

• Department of Computer Science York University Toronto, Canada,