Skip to content

Commit 4ca460a

Browse files
roberthoenigroberthoenig
committed
Initial commit.
Add source files, tests, and basic README.
1 parent 9199464 commit 4ca460a

24 files changed

+946
-4
lines changed

‎.gitignore‎

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -1,3 +1,4 @@
11
*.jl.cov
22
*.jl.*.cov
33
*.jl.mem
4+
coverage

‎README.md‎

Lines changed: 2 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -1 +1,3 @@
11
# FirstOrderLogic
2+
3+
This is a Julia package for parsing, manipulating and evaluating formulas in first-order logic.

‎REQUIRE‎

Lines changed: 2 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -1 +1,3 @@
11
julia 0.6
2+
Match
3+
AutoHashEquals

‎src/FirstOrderLogic.jl‎

Lines changed: 19 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -1,5 +1,22 @@
1+
__precompile__()
12
module FirstOrderLogic
23

3-
# package code goes here
4+
using AutoHashEquals
5+
using Match
46

5-
end # module
7+
# Declarative and supportive code.
8+
include("types.jl")
9+
include("helpers.jl")
10+
include("testing_helpers.jl")
11+
12+
# Workhorse code.
13+
include("parser.jl")
14+
include("renamed_quantifiers_form.jl")
15+
include("quantified_variables_form.jl")
16+
include("prenex_normal_form.jl")
17+
include("skolem_normal_form.jl")
18+
include("conjunctive_normal_form.jl")
19+
include("removed_quantifier_form.jl")
20+
include("resolution.jl")
21+
22+
end

‎src/conjunctive_normal_form.jl‎

Lines changed: 65 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,65 @@
1+
export get_conjunctive_normal_form
2+
3+
"""
4+
Get equivalent formula in the conjunctive normal form for a given formula.
5+
"""
6+
function get_conjunctive_normal_form(formula)
7+
# Ideally, we would use a single @match clause to handle both
8+
# negations and junctions. The negation case is tricky to implement
9+
# in such a unified approach, however, so we generate the CNF in two
10+
# steps.
11+
"""
12+
Get equivalent formula with no negation in non-literal formulas.
13+
"""
14+
function collapse_negations(formula)
15+
@match formula begin
16+
f::Negation => begin
17+
@match f.formula begin
18+
ff::Negation => collapse_negations(ff.formula)
19+
ff::Conjunction || ff::Disjunction => begin
20+
opposite_type = typeof(ff) == Conjunction ? Disjunction : Conjunction
21+
opposite_type(
22+
collapse_negations(Negation(ff.formula1)),
23+
collapse_negations(Negation(ff.formula2)),
24+
)
25+
end
26+
ff::AtomicFormula => f
27+
end
28+
end
29+
f::Conjunction || f::Disjunction => typeof(f)(
30+
collapse_negations(f.formula1),
31+
collapse_negations(f.formula2),
32+
)
33+
f::AtomicFormula => f
34+
_ => throw(TypeError(:collapse_negations, "", Formula, typeof(formula)))
35+
end
36+
end
37+
function expand_disjunctions(formula)
38+
obj = @match formula begin
39+
f::Disjunction => begin
40+
cnf1 = expand_disjunctions(f.formula1)
41+
cnf2 = expand_disjunctions(f.formula2)
42+
# Concatenate the clauses in each pair of the cartesian product and
43+
# return the whole thing as a vector of clauses (that is, in CNF).
44+
resultcnf = CNF()
45+
for clause1 in cnf1
46+
for clause2 in cnf2
47+
newclause = union(clause1, clause2)
48+
push!(resultcnf, newclause)
49+
end
50+
end
51+
resultcnf
52+
end
53+
f::Conjunction => begin
54+
clauses = union(expand_disjunctions(f.formula1),
55+
expand_disjunctions(f.formula2))
56+
CNF(clauses)
57+
end
58+
f::AtomicFormula => CNF([Clause([Literal(false, f)])])
59+
f::Negation => CNF([Clause([Literal(true, f.formula)])])
60+
end
61+
return obj
62+
end
63+
collapsed_formula = collapse_negations(formula)
64+
expand_disjunctions(collapsed_formula)
65+
end

‎src/helpers.jl‎

Lines changed: 151 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,151 @@
1+
export @debug
2+
# reshape
3+
4+
function bracketsplit(str)
5+
parts = []
6+
part_start = 1
7+
bracket_balance = 0
8+
for idx in eachindex(str)
9+
bracket_balance += @match str[idx] begin
10+
'(' => -1
11+
')' => 1
12+
_ => 0
13+
end
14+
if bracket_balance == 0
15+
push!(parts, str[part_start:idx])
16+
part_start = idx+1
17+
end
18+
end
19+
parts
20+
end
21+
22+
function argumentsplit(str)
23+
parts = strip.(bracketsplit(str))
24+
comma = findfirst(parts, ",")
25+
if comma == 0
26+
[str]
27+
else
28+
arguments = [join(parts[1:comma-1])]
29+
while comma != 0
30+
next_comma = findnext(parts, ",", comma+1)
31+
if next_comma == 0
32+
push!(arguments, join(parts[comma+1:end]))
33+
else
34+
push!(arguments, join(parts[comma+1:next_comma-1]))
35+
end
36+
comma = next_comma
37+
end
38+
arguments
39+
end
40+
end
41+
42+
function strip_and_remove_surrounding_brackets(str)
43+
str = strip(str)
44+
while length(bracketsplit(str)) == 1 && str[1] == '('
45+
str = str[2:end-1]
46+
end
47+
str
48+
end
49+
50+
function powerset(x)
51+
result = [Set()]
52+
# println("collect(x) ", collect(x))
53+
for element in collect(x), idx = 1:length(result)
54+
# println("element ", element)
55+
# println("idx ", idx)
56+
newsubset = union(result[idx], Set([element]))
57+
push!(result, newsubset)
58+
end
59+
Set(result)
60+
end
61+
62+
# Currently, Julia's multiple dispatch system only dispatches on the expression type for
63+
# macros (which is most of the times Expr or Symbol). To do multiple dispatch here, we
64+
# therefore have to work around that limitation by using the hack below. This might change
65+
# if https://github.com/JuliaLang/julia/issues/20929 gets addressed.
66+
macro applyrecursively(functionexpr, objectexpr, objecttype)
67+
typemapping = Dict(
68+
:CNF => :collection,
69+
:Clause => :collection,
70+
:Conjunction => :monotone_fields,
71+
:Negation => :monotone_fields,
72+
)
73+
dispatch_applyrecursively(functionexpr, objectexpr, Val{typemapping[objecttype]})
74+
end
75+
76+
function dispatch_applyrecursively(functionexpr, objectexpr,
77+
objecttype::Type{Val{:collection}})
78+
fsymbol, fargs = functionexpr.args[1],
79+
functionexpr.args[2:end]
80+
quote
81+
obj = $(esc(objectexpr))
82+
typeof(obj)(
83+
[$fsymbol([arg == :_ ? element : arg
84+
for arg in [$(esc.(fargs)...)]]...)
85+
for element in obj]
86+
)
87+
end
88+
end
89+
90+
# function dispatch_applyrecursively(functionexpr, objectexpr,
91+
# objecttype::Type{Val{:monotone_fields}})
92+
# fsymbol, fargs = functionexpr.args[1],
93+
# functionexpr.args[2:end]
94+
# quote
95+
# typeof($(esc(objectexpr)))(
96+
# [$fsymbol(
97+
# [arg == :_ ? field : arg
98+
# for arg in $(esc(fargs))]...)
99+
# for field in getfield.($(esc(objectexpr)), fieldnames($(esc(objectexpr))))]...)
100+
# end
101+
# end
102+
103+
macro debug(variable)
104+
Expr(:call,
105+
:println,
106+
Expr(:call,
107+
:string,
108+
Expr(:quote, variable)),
109+
" ",
110+
esc(variable),
111+
"\n"
112+
)
113+
end
114+
print(args...) = println(args...)
115+
116+
let nextfreesymbol = 0
117+
global getnextfreesymbol
118+
global resetfreesymbols
119+
function getnextfreesymbol()
120+
nextfreesymbol += 1
121+
string("##", nextfreesymbol)
122+
end
123+
function resetfreesymbols()
124+
nextfreesymbol = 0
125+
end
126+
end
127+
128+
# function reshape(formula::String, form::FormulaForm)
129+
# form == string ? String(Formula(formula)) : reshape(Formula(formula))
130+
# end
131+
132+
# function reshape(formula::Formula, form::FormulaForm)
133+
# @match form begin
134+
# string => String(formula)
135+
# formula => formula
136+
# quantifiedvariables => get_quantified_variables_form(formula)
137+
# prenex => get_prenex_normal_form(formula)
138+
# skolem => get_prenex_normal_form(
139+
# get_skolem_normal_form(formula)
140+
# )
141+
# removedquantifier => get_removed_quantifier_form(formula)
142+
# conjunctive => get_conjunctive_normal_form(formula)
143+
# resolutionready => get_conjunctive_normal_form(
144+
# get_removed_quantifier_form(
145+
# get_skolem_normal_form(
146+
# get_prenex_normal_form(
147+
# get_quantified_variables_form(
148+
# Formula(formula)))))
149+
# )
150+
# end
151+
# end

‎src/parser.jl‎

Lines changed: 62 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,62 @@
1+
Term(str::AbstractString) = begin
2+
function get_term(str)
3+
function_match = match(r"(\w*)\((.*)\)$", str)
4+
if function_match == nothing
5+
Variable(strip(str))
6+
else
7+
name = strip(function_match.captures[1])
8+
arguments = get_term.(argumentsplit(strip(function_match.captures[2])))
9+
Function(FunctionSymbol(name), arguments)
10+
end
11+
end
12+
get_term(str)
13+
end
14+
15+
AtomicFormula(str::AbstractString) = begin
16+
formula = strip_and_remove_surrounding_brackets(str)
17+
atomic_formula_match = match(r"(\w*)\((.*)\)$", formula)
18+
name = strip(atomic_formula_match.captures[1])
19+
arguments = Term.(argumentsplit(strip(atomic_formula_match.captures[2])))
20+
AtomicFormula(PredicateSymbol(name), arguments)
21+
end
22+
23+
Negation(str::AbstractString) = begin
24+
Negation(Formula(str[2:end]))
25+
end
26+
27+
EFormula(str::AbstractString) = begin
28+
e_formula_match = match(r"\?\{(\w+)\}(.*)", str)
29+
name = strip(e_formula_match.captures[1])
30+
formula = strip(e_formula_match.captures[2])
31+
EFormula(Variable(name), Formula(formula))
32+
end
33+
34+
AFormula(str::AbstractString) = begin
35+
a_formula_match = match(r"\*\{(\w+)\}(.*)", str)
36+
name = strip(a_formula_match.captures[1])
37+
formula = strip(a_formula_match.captures[2])
38+
AFormula(Variable(name), Formula(formula))
39+
end
40+
41+
Formula(str::AbstractString) = begin
42+
formula = strip_and_remove_surrounding_brackets(str)
43+
parts = strip.(bracketsplit(formula))
44+
previous_junction = 0
45+
current_junction = findfirst(part->ismatch(r"^[&|]$", part), parts)
46+
if current_junction == 0
47+
@match formula[1] begin
48+
'?' => return EFormula(formula)
49+
'*' => return AFormula(formula)
50+
'~' => return Negation(formula)
51+
_ => return AtomicFormula(formula)
52+
end
53+
else
54+
formula1 = strip(join(parts[previous_junction+1:current_junction-1]))
55+
operator = strip(join(parts[current_junction]))
56+
formula2 = strip(join(parts[current_junction+1:end]))
57+
@match operator begin
58+
"&" => return Conjunction(Formula(join(formula1)), Formula(formula2))
59+
"|" => return Disjunction(Formula(formula1), Formula(formula2))
60+
end
61+
end
62+
end

‎src/prenex_normal_form.jl‎

Lines changed: 41 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,41 @@
1+
export get_prenex_normal_form
2+
3+
function handle_negation(formula)
4+
result = @match formula begin
5+
f::AFormula => EFormula(f.variable, handle_negation(f.formula))
6+
f::EFormula => AFormula(f.variable, handle_negation(f.formula))
7+
_ => Negation(formula)
8+
end
9+
return result
10+
end
11+
12+
function handle_junction(formula1, formula2, junction)
13+
if typeof(formula1) in (AFormula, EFormula)
14+
return typeof(formula1)(
15+
formula1.variable,
16+
handle_junction(formula1.formula, formula2, junction),
17+
)
18+
elseif typeof(formula2) in (AFormula, EFormula)
19+
return typeof(formula2)(
20+
formula2.variable,
21+
handle_junction(formula1, formula2.formula, junction),
22+
)
23+
else
24+
return junction(formula1, formula2)
25+
end
26+
end
27+
28+
function get_prenex_normal_form(formula)
29+
prepared_formula = get_renamed_quantifiers_form(formula)
30+
@match prepared_formula begin
31+
f::Negation => handle_negation(
32+
get_prenex_normal_form(f.formula),
33+
)
34+
f::Conjunction || f::Disjunction => handle_junction(
35+
get_prenex_normal_form(f.formula1),
36+
get_prenex_normal_form(f.formula2),
37+
typeof(f),
38+
)
39+
_ => return formula
40+
end
41+
end

‎src/quantified_variables_form.jl‎

Lines changed: 29 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,29 @@
1+
export get_quantified_variables_form,
2+
get_unbound_variables
3+
4+
function get_quantified_variables_form(formula)
5+
variables = get_unbound_variables(formula)
6+
quantified_variables_form = formula
7+
for variable in variables
8+
quantified_variables_form = EFormula(variable, quantified_variables_form)
9+
end
10+
quantified_variables_form
11+
end
12+
13+
function get_unbound_variables(formula, boundvars=Set{Variable}())
14+
@match formula begin
15+
f::Conjunction || f::Disjunction => begin
16+
unboundvars = get_unbound_variables.([f.formula1, f.formula2], boundvars)
17+
union(unboundvars...)
18+
end
19+
f::Negation => get_unbound_variables(f.formula, boundvars)
20+
f::AFormula || f::EFormula => begin
21+
push!(boundvars, f.variable)
22+
unboundvars = get_unbound_variables(f.formula, boundvars)
23+
pop!(boundvars, f.variable)
24+
unboundvars
25+
end
26+
f::AtomicFormula || f::Function => union(get_unbound_variables.(f.arguments, boundvars)...)
27+
f::Variable => f in boundvars ? Set() : Set([f])
28+
end
29+
end

0 commit comments

Comments
 (0)