FirstOrderLogic.jl | Overview | Installation | Usage | Why not PROLOG? | Roadmap
This is a Julia package for parsing, manipulating and evaluating formulas in first-order logic. It may prove useful to
For example, to check if ∀x(P(x) ∧ ¬P(f(x)))
is unsatisfiable, run
is_satisfiable("*{x}(P(x) & ~P(f(x)))")
Linux | Windows | Coverage |
---|---|---|
FirstOrderLogic.jl
follows the standard structure for Julia projects.
Currently, it provides the following:
An intuitive type system for formulas in first-order logic.
Various methods for converting formulas in special forms:
A prover for formulas in first-order logic.
julia
Pkg.clone("git@github.com:roberthoenig/FirstOrderLogic.jl.git")
Say we have a formula ∀x(P(x) ∧ ¬P(f(x)))
. We want to verify that this formula is unsatisfiable.
To do so, we do the following:
FirstOrderLogic.jl
syntax: *{x}(P(x) & P(f(x)))
.julia
FirstOrderLogic.jl
:
using FirstOrderLogic
is_satisfiable(<our formula>)
:
is_satisfiable("*{x}(P(x) & ~P(f(x)))")
If everything works correctly, the program should print "false" and terminate. This means that ∀x(P(x) ∧ ¬P(f(x)))
is unsatisfiable. We have verified what we wanted to verify.
FirstOrderLogic.jl
currently uses its own syntax for representing formulas
in first-order logic. A parser for latex symbols is in progress.
The following is a list of all currently supported syntactic elements.
Mathematical syntax | FirstOrderLogic.jl syntax |
Semantic |
---|---|---|
x | x | variable |
f(x,y) | f(x,y) | function |
f(x,y) | f(x,y) | predicate |
∃x | ?{x} | existential quantification |
∀x | *{x} | universal quantification |
¬x | ~x | negation |
x ∧ y | x & y | conjunction |
x ∨ y | x | y | disjunction |
x → y | x > y | implication |
(x ∧ y) ∨ z | (x & y) | z | precedence grouping |
Formula in mathematical notation:
∀x∃yA(x,g(y,z)) ∧ (¬B() ∨ ∃dC(d))
The same formula in FirstOrderLogic.jl
notation:
*{x}?{y}A(x,g(y,z)) & (~B() | ?{d}C(d))
Function | Purpose |
---|---|
is_satisfiable(formula; maxsearchdepth) |
Checks if formula is satisfiable. |
get_conjunctive_normal_form(formula) |
Returns formula in the conjunctive normal form, expressed as clauses. |
get_prenex_normal_form(formula) |
Returns the prenex normal form of formula . |
get_skolem_normal_form(formula) |
Returns the skolem normal form of formula . |
Formula(str) |
Parse str to a Formula object and return that object. |
Each available function comes with a concise docstring.
The PROLOG programming language can be used to prove seemingly arbitrary statements in first-order logic. PROLOG differs from FirstOrderLogic.jl
in two ways:
FirstOrderLogic.jl
uses a direct
mathematical syntax for expressing formulas.FirstOrderLogic.jl
does not make that trade. It is slow, but complete.The following features are work in progress:
is_satisfiable()
.is_satisfiable()
.Any and all external contributions are most welcome!