8 Tableaux Implemented

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

• 8.1 Implementing PLNQ
  • 8.1.1 Literals
  • 8.1.2 Complex Formulae: Negation
  • 8.1.3 Complex Formulae: Conjunctive Expansion
  • 8.1.4 Complex Formulae: Disjunctive Expansion
  • 8.1.5 An Example - first Steps
  • 8.1.6 An Example - final Step
  • 8.1.7 Another Example
  • 8.1.8 Two Connectives

• 8.2 Wrapping it up (Theorem Proving)

• 8.3 Exercises