Automated reasoning in non-classical logics with the polarized inverse method

Опубликовано 7 сентября 2016, 17:32

Automated reasoning in classical logic has received much attention in the literature. Mature resolution theorem provers such as Vampire and E can handle enormous problems in first-order classical logic with equality. Waldmeister, a theorem prover for unit equational logic, has been incorporated into Mathematica as an equational reasoning method. Somewhat surprisingly, there has been much less attention devoted to non-classical logics. This is unfortunate, since many interesting and useful logics are inherently non-classical. Well known examples include intuitionistic, substructural and modal logics. Additionally, many modern logics for specialized tasks such as those designed for security and authentication protocols are non-classical as well. The inverse method is a generalization of resolution to non-classical logics. The polarized inverse method extends the inverse method with focusing and explicit polarity assignments that dramatically decrease the search space. In this talk we will suggest that the polarized inverse method provides an efficient and flexible framework for implementing theorem provers for non-classical logics. As evidence, we will demonstrate our recent theorem prover for intuitionistic logic, named Imogen. Imogen performs better than any other intuitionistic prover on standard benchmarks. We will also discuss recent work extending Imogen to handle domain-specific reasoning such as Microsoft's Infon logic. Finally, we will introduce a recent technique for encoding substructural logics into intuitionistic logic, thus yielding theorem provers for these logics for