# Labs 04: LCF Approach

### Directory structure

. ├── 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

### Project description

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.

### Preamble

#### Normal form checking

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

#### Converting formulas to normal form

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.

#### Proving lemmas

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

### Proving equivalence between formulas and their normal forms

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.