skolemizer ~main

A Skolemization library for first-order logic formulas


To use this package, run the following command in your project's root directory:

Manual usage
Put the following dependency into your project's dependences section:

InfoReference

How to run: type a formula into input.txt making sure to use the following syntax:

  • | Conjunction
  • & Disjunction
  • ! Negation
  • = Biconditional
  • > Implication
  • A Universal Quantifier
  • E Existential Quantifier
  • Any lowercase letter for a variable
  • Any uppercase letter (other than A and E) for a predicate

Example: AxEyAz(P(x,y,z) & Q(x,y,z) > R(y)) is a valid formula

After that, type dub run into the terminal and then check out ast.txt and skolemized_ast.txt

Example output with input (AxP(s(s(s(s(s(s(x))))))) & EyP(y) & AzP(z) & EwP(w)): P(s(s(s(s(s(s(v0))))))) ∧ P(f0(v0)) ∧ P(v2) ∧ P(f1(v0,v2))

Authors:
  • Zachary A. Davis
Dependencies:
none
Versions:
1.0.9 2026-Apr-13
1.0.8 2026-Apr-13
1.0.7 2026-Apr-08
1.0.6 2026-Apr-08
1.0.5 2026-Apr-08
Show all 11 versions
Download Stats:

  • 0 downloads today

  • 0 downloads this week

  • 2 downloads this month

  • 38 downloads total

Score:
0.0
Short URL:
skolemizer.dub.pm