Easy-to-use first order logic tools.

• Formula transformations
  • Express in terms of AND, OR, NOT
  • De Morgan's laws
  • Quantifier negation
  • Conjunctive normal form (CNF)
  • Prenex normal form (PNF)
  • Substitute variables, etc.
• Skolemization
  • Substitute Skolem's function
• Unification
  • Most general unifier (MGU)
• Semantic tableaux method (MTS)
• Resolution method
• CLI client
• Web client

sbt run

sbt ~test

Qu      → ∀ | ∃
Op      → ∧ | ∨ | …
Id      → [a-z]+[0-9]*[']*
Con     → @Id
Var     → Id
Func    → Id
Pred    → Id

Args    → Term | Term, Args → List(Term)
Term    → Con | Var | Func(Args)
Atom    → Pred(Args)
Form    → Atom | ¬Form | Form Op Form | Qu Var Form
Literal → Atom | ¬Atom
Clause  → Literal ∨ Literal