Methods for Automated Theorem Proving in Nonclassical Logics

   Info_icon.svg       BibTeX_logo.svg   
Charles G. Morgan
IEEE Transactions on Computers C-25(8), pp. 852–862
agosto 1976

In this paper we outline two basic methods for automated theorem proving in nonclassical logics, including modal, many-valued, relevance, and intuitionistic logics. We discuss advantages and disadvantages of each method and give several illustrative examples. We outline a procedure for attacking more complex problems using a combination of the two basic methods. Results of experimental applications of the techniques are reported.

rivista o collana
Journal_icon.svg IEEE Transactions on Computers (TC)