Understanding your Assignment brief

Assignment summary:

Automated theorem proving (ATP) is an automated process of mathematical and logical reasoning, dealing with proofs of mathematical theorems executed by computers. The introduction of ATP is considered as a milestone for the development and reasoning of computer systems, as it enables their analysis using the robustness and power of mathematics.

ATP was developed through the study of formal languages that are used to analyse, in a rigorous way, a wide range of reasoning problems with respect to computer systems. For the use of ATP, inference rules have been developed to enable the drawing of sound and correct conclusions from given mathematical statements related to the system under examination.

Performing ATP
As has already been mentioned, theorem proving is an automated process that uses computers to reason the systems under examination. Specifically, this process is conducted using computer programs called theorem provers. These programs facilitate the development and analysis of a system’s behaviour in a formal logic, which consists of the following elements:

• A formal language that is used to express formulas

• The axioms, which are a set of formulas

• The inference rules that are used for the derivation of new formulas or axioms out of the existing ones

In the formal logic, the reasoning about mathematical problems relies on logic propositions (ie formulas) that describe the validity of the axioms by providing evidence about their truth. Moreover, inference rules are used to preserve this validity throughout the proving process.

Thus, the application of inference rules should ensure that the new axioms and formulas derived from the initial axioms are also valid, as happens with all the mathematical proofs. Usually, inference rules and axioms are used to prove theorems (ie general mathematical propositions) through a sequence of logical steps. The outcome that is obtained by following these steps is called derivation or deduction. In theorem proving, a theorem prover is used to verify a formula by showing that the deduction of that formula is following a logic that proves that is truth.

Having described how theorem proving works in general, we need to explain how it can be used to check the correctness of a computer system. As in mathematics, in theorem proving we construct a formula that defines the correctness of the system to be examined, considering it as the theorem to be proved. Then, following the logic of a theorem prover, along with the respective inference rules, we try to obtain a deduction that proves the correctness of the system’s behaviour.

Note that a formal proof of a theorem that is related to the correctness of a computer system usually requires time, discipline and attention to detail as the formulas to be proved may be extremely long and complicated.

Assignment Requirements

Explore this verification technique further and then post at least one applicability, one advantage and one disadvantage when prompted in the next step. You will then be asked to peer review a fellow student’s submission, providing feedback based on the assignment guidelines listed further below. This assignment contains 1 part. In the submission step you will be asked to submit 1 item. For each criterion you will receive either 1 point or 0 point, depending on whether your marker feels you have evidenced the criterion or not.

Task Prompt 1: Explore Automated Theorem Proving further and identify at least one applicability, one advantage and one disadvantage.

This first Prompt is graded against the following criteria:

Criteria 1: Has the learner described at least one applicability?
Criteria 2: Has the learner described at least one advantage?
Criteria 3: Has the learner described at least one disadvantage?

The next step is where you’ll submit your responses to these Task Prompts. You need to submit them all at the same time, so don’t start until you’re ready.

You may choose to actually draft your work there, but you may wish to work offline or in a separate tab or document to perfect your ideas before you submit and share with your course peers.

Please note – you’ll be prompted to give your assignment an overall descriptive title. It’s your chance to get creative, or you could keep this simple and descriptive.