Propositional Logic Link to heading
In this short post we will explore how different proof strategies, particularly in backwards reasoning, can impact the efficiency of deriving conclusions. At the end, I’ll include a table of Paulson’s rules for the folderol theorem prover.
Propositional logic works with the connectives \(\land\), \(\lor\), \(\to\), \(\leftrightarrow\), and \(\neg\).
Instead of defining \(\neg A\) as \(A \to \bot\), we treat \(\neg\) as a basic operator on its own.
In backwards proof, we break down complex conclusions step by step. The challenge is in choosing the most efficient path through the rules, as some routes can lead to significantly shorter proofs than others.
Example
Consider the simple example of proving: \(A \land B \vdash B \land A\). Two different proofs below illustrate this.
Proof 1
\(\displaystyle \cfrac {\cfrac {A, B \vdash B}{A \land B \vdash B} \quad (\land L) \qquad \cfrac {A, B \vdash A}{A \land B \vdash A} \quad (\land L)}{A \land B \vdash B \land A} \quad (\land R)\)
As you can see, if \(\land R\) is used first then \(\land L\) must be used twice.
Proof 2
\(\displaystyle \cfrac {\cfrac {A, B \vdash B \qquad A, B \vdash A}{A, B \vdash B \land A} \quad (\land R)}{A \land B \vdash B \land A} \quad (\land L)\)
The second proof is shorter because we used \(\land L\) first.
Rules can be chosen to limit subgoal creation. If a goal is a basic sequent, using other rules is pointless. The cost of a rule is the number of premises: 1-premise rules are cheaper than 2-premise ones. Therefore in the above example \(\land L\) is cheaper than \(\land R\).
We will represent a goal in our theorem prover by a list of triples. Each triple includes:
- Formula – Id of the specific formula.
- Side – Indicates whether the formula is on the left side or the right side of the sequent.
- Cost – The “cost” associated with applying the rule related to this formula.
Rules Link to heading
Finally here are the summary for our rules of propositional logic and quantifiers.
Propositional Logic Rules
| Rule L | Rule R |
|---|---|
| \(\displaystyle \cfrac {A, B \vdash}{A \land B \vdash} \quad (\land L)\) | \(\displaystyle \cfrac {\vdash A \quad \vdash B}{\vdash A \land B} \quad (\land R)\) |
| \(\displaystyle \cfrac {A \vdash \quad B \vdash}{A \lor B \vdash} \quad (\lor L)\) | \(\displaystyle \cfrac {\vdash A, B}{\vdash A \lor B} \quad (\lor R)\) |
| \(\displaystyle \cfrac {\vdash A \quad B \vdash}{A \rightarrow B \vdash} \quad (\rightarrow L)\) | \(\displaystyle \cfrac {A \vdash B}{\vdash A \rightarrow B} \quad (\rightarrow R)\) |
| \(\displaystyle \cfrac {A, B \vdash \quad \vdash A, B}{A \leftrightarrow B \vdash} \quad (\leftrightarrow L)\) | \(\displaystyle \cfrac {A \vdash B \quad B \vdash A}{\vdash A \leftrightarrow B} \quad (\leftrightarrow R)\) |
| \(\displaystyle \cfrac {\vdash A}{\neg A\vdash} \quad (\neg L)\) | \(\displaystyle \cfrac {A \vdash}{\vdash \neg A} \quad (\neg R)\) |
Quantifier Rules
Here \(t\) stands for term, \(a\) is a parameter and \(x\) is some arbitrary value.
| Rule L | Rule R |
|---|---|
| \(\displaystyle {\cfrac {\forall x.A,A[t/x]\vdash }{\forall x.A\vdash }}\quad (\forall L)\) | \(\displaystyle {\cfrac {\vdash A[a/x]}{\vdash \forall x.A}}\quad (\forall R) \star\) |
| \(\displaystyle {\cfrac {A[a/x] \vdash}{\exists x.A \vdash}}\quad (\exists L) \star\) | \(\displaystyle {\cfrac {\vdash \exists x.A, A[t/x]}{\vdash \exists x.A}}\quad (\exists R)\) |
\(\star\) Note that in rules \((\exists L)\) and \((\forall R)\) parameter \(a\) must not appear in the conclusion (\(A\)).
In the next post we’ll take a brief look at quantifiers and unification ;)