6 Tableaux Implemented

In this chapter, we present an implementation of the tableaux algorithm we've presented in the last chapter.

• 6.1 Implementing PLNQ
  • 6.1.1 Literals
  • 6.1.2 Complex Formulae: Negation
  • 6.1.3 Complex Formulae: Conjunctive Expansion
  • 6.1.4 Complex Formulae: Disjunctive Expansion
  • 6.1.5 An Example - first Steps
  • 6.1.6 An Example - final Step
  • 6.1.7 Another Example
  • 6.1.8 Two Connectives

• 6.2 Wrapping it up (Theorem Proving)