An Overview of Automated Theorem Provers at Advanced Course of Applied Logics at Tallinn University of Technology

Today is a due date for presenting a completed assignment at university. The course is Advanced Course of Applied Logics and its mandatory assignment is an overview of Automated Theorem Provers. The meaning of Automated Theorem Provers (ATP) is clarified, if it is known what Automated Theorem Proving means. Particularly, it is the proving of some statement (theorem) on the basis of previously proved (other theorems) or accepted other statements (axioms).

To be more specific, there are the hypothesis and the conclusion. The hypothesis is known as the premise and served as an input to the proving. The conclusion is known as the logical consequence and served as it has to be at an output from the proving. If the hypothesis is true then the conclusion must also be true. For this reason, provers produce inference steps, taking into consideration the hypothesis. The proving is successful when finished with a certain result that the conclusion is a consequence of the hypothesis.

Automated theorem provers deal with the proving expressed using formal languages or logical signatures. Theorems are considered as statements of a formal language. Formal language in turn considers formal logic. Although it may differ significantly from one prover to another, common fixed formal logic is usually shared. An assumption is that such a formal logic is first-order logic. This one is classical logic, which is an extension of propositional logic. A bunch of other classical logics includes second-order logic and higher-order logic. The former is an extension of first-order logic and the latter is an extension of second-order logic. Alternatively, non-classical and modal logic can also be used.

Today, the most typical widely used logic is first-order logic. There are several reasons for this assumption. As well as being used in many scientific fields and studies, it has become the standard logic for scientific subjective systems. Its syntax involves only finite (boolean) expressions and quantification with the forbiddance to quantify over predicates. Moreover, the existence of a wide range of problems for this logic makes more well developed theorem proving. Consequently, first-order logic is emphasized by this overview.

As for an availability of automated theorem provers, there is a vast variety of them nowadays. However, when a problem for the proving was asserted, certain requirements could be made for them. It is further considered that the requirement is first-order logic. In this field, both free software and proprietary software have already been developed. The important software systems are probably those, which had been invented first then on its basis another systems were established and they proved the ability for solving “real” problems of a different scale. Such a one opportunity to prove is the CADE ATP System Competition (CASC). E equational theorem prover, Otter and Prover9 are demonstrated as an example.

Otter theorem prover had been widely utilized at first for first-order and equational logic. Then Otter was substituted by Prover9.

E is a purely equational theorem prover for full first-order logic with equality. It is integrated into other theorem provers. Moreover, it has won several categories in the CADE ATP System Competition.

That is all for this overview. May be liked it and a try with provers will be held.

References

Tags: ,

Comments are closed.