Methods for Automated Theorem Proving in Nonclassical Logics

   page       BibTeX_logo.png   
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.