Download the archive: labs04.tar.gz

.
├── build.sbt
├── fol
│   ├── lib
│   │   └── scallion_2.12-0.3.jar
│   └── src
│       └── main
│           └── scala
│               └── fol
│                   ├── Formulas.scala // Definitions of expressions and formulas
│                   ├── package.scala
│                   ├── parser
│                   └── Utils.scala
├── lcf
│   └── src
│       └── main
│           └── scala
│               └── lcf
│                   └── package.scala // LCF rules and axioms
├── project
│   └── build.properties
└── src
    └── main
        └── scala
            ├── Main.scala
            ├── Project.scala // Normalization and proof of correctness
            ├── Tests.scala
            └── Theorems.scala // Theorems derived from the axioms

The goal of this lab is to convert first-order logic formulas to normal forms, and prove that formulas are equivalent to their normal forms. The LCF rules and axioms are given in the file package.scala of the lcf project. You are provided with theorems that follow from these rules and axioms in the file Theorems.scala, which will be useful later on. Look carefully at all the axioms and theorems provided to you, they will be helpful for the lab.

Be sure to familiarize yourself with the syntax for describing formulas by reading the documentation and by looking at the definitions in Theorems.scala. The documentation also contains the definitions for formulas and the descriptions of all rules and axioms.

In Project.scala, complete the function isNormalForm that checks that a formula only contains implications, equalities, predicates, False, and forall quantifiers.

In Project.scala, complete the function toNormalForm that converts a formula to an equivalent formula in normal form that satisfies isNormalForm predicate.

To do this, make use of the fact that implication along with False can express all other propositional connectives, e.g. Not(p) is Implies(p, False), and Or(p,q) is Implies(Not(p), q). Furthermore, Exists can be expressed using Not and forall.

In Theorems.scala, prove the lemmas modusPonensThm, iffSym and iffTrans which can be useful for the next step.

After completing the preamble, we will now prove that the conversion to normal form is correct. In Project.scala, complete the function toNormalFormThm that given a formula f returns a theorem stating that f is equivalent to its normal form.