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:

dub.json

dub.sdl

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))

~main released 8 hours ago
3zad/skolemizer-core
proprietary
Copyright © 2026, Zachary A. Davis

Authors:

Zachary A. Davis

Dependencies:

none

Versions:

1.0.2	2026-Mar-30
1.0.1	2026-Mar-30
1.0.0	2026-Mar-30
~main	2026-Mar-30

Download Stats:

5 downloads today
5 downloads this week
5 downloads this month
5 downloads total

Score:

Short URL:

skolemizer.dub.pm