Automated theorem proving by resolution in non-classical logics

DOI10.1007/S10472-007-9051-8MaRDI QIDQ2385426zbMATH OpenOpenAlexFDO

Authors Viorica Sofronie-Stokkermans

Publication date 12 October 2007

Published in Annals of Mathematics and Artificial Intelligence (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/s10472-007-9051-8

zbMATH Keywords

automated theorem proving decision procedures nonclassical logic resolution principle

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35)

Review text

The main goal of the paper is to find uniform principles, applicable to large classes, which lead to simple and reusable implementations. The author presents several situations in which nonclassical logics can be translated into tractable and simple fragments of classical logic and resolution can be used successfully for automated theorem proving. The main advantage of such an approach is that it allows one to use existing automated theorem provers. She shows in this paper that in many interesting situations translations into classical logic allows one to obtain decision procedures of optimal complexity. Such resolution-based decision procedures can be obtained by using refinements of resolution such as ordered resolutionn with selection, or ordered chaining with selection.

Recommendations

Cites work

Cited in

(25)

This page was built for publication: Automated theorem proving by resolution in non-classical logics

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2385426)