Proving Propositional Logic Statements

using Test
using Metatheory
using TermInterface

# Rewriting

fold = @theory p q begin
(p::Bool == q::Bool) => (p == q)
(p::Bool || q::Bool) => (p || q)
(p::Bool ⟹ q::Bool)  => ((p || q) == q)
(p::Bool && q::Bool) => (p && q)
!(p::Bool)           => (!p)
end

or_alg = @theory p q r begin
((p || q) || r) == (p || (q || r))
(p || q) == (q || p)
(p || p) --> p
(p || true) --> true
(p || false) --> p
end

and_alg = @theory p q r begin
((p && q) && r) == (p && (q && r))
(p && q) == (q && p)
(p && p) --> p
(p && true) --> p
(p && false) --> false
end

comb = @theory p q r begin

DeMorgan

  !(p || q) == (!p && !q)
!(p && q) == (!p || !q)

distrib

  (p && (q || r)) == ((p && q) || (p && r))
(p || (q && r)) == ((p || q) && (p || r))

absorb

  (p && (p || q)) --> p
(p || (p && q)) --> p

complement

  (p && (!p || q)) --> p && q
(p || (!p && q)) --> p || q
end

negt = @theory p begin
(p && !p) --> false
(p || !(p)) --> true
!(!p) == p
end

impl = @theory p q begin
(p == !p) --> false
(p == p) --> true
(p == q) --> (!p || q) && (!q || p)
(p ⟹ q) --> (!p || q)
end

propositional_logic_theory = or_alg ∪ and_alg ∪ comb ∪ negt ∪ impl ∪ fold

Sketch function for basic iterative saturation and extraction

function prove(
t,
ex,
steps = 1,
timeout = 10,
params = SaturationParams(
timeout = timeout,
scheduler = Schedulers.BackoffScheduler,
schedulerparams = (6000, 5),
timer = false,
),
)
hist = UInt64[]
push!(hist, hash(ex))
for i in 1:steps
g = EGraph(ex)

exprs = [true, g[g.root]]
ids = [addexpr!(g, e) for e in exprs]

goal = (g::EGraph) -> in_same_class(g, ids...)
params.goal = goal
saturate!(g, t, params)
ex = extract!(g, astsize)
if !Metatheory.istree(ex)
return ex
end
if hash(ex) ∈ hist
return ex
end
push!(hist, hash(ex))
end
return ex
end

@testset "Prop logic" begin
ex = rewrite(:(((p ⟹ q) && (r ⟹ s) && (p || r)) ⟹ (q || s)), impl)
@test prove(propositional_logic_theory, ex, 5, 10, 5000)

@test @areequal propositional_logic_theory true ((!p == p) == false)
@test @areequal propositional_logic_theory true ((!p == !p) == true)
@test @areequal propositional_logic_theory true ((!p || !p) == !p) (!p || p) !(!p && p)
@test @areequal propositional_logic_theory p (p || p)
@test @areequal propositional_logic_theory true ((p ⟹ (p || p)))
@test @areequal propositional_logic_theory true ((p ⟹ (p || p)) == ((!(p) && q) ⟹ q)) == true

Frege's theorem

  @test @areequal propositional_logic_theory true (p ⟹ (q ⟹ r)) ⟹ ((p ⟹ q) ⟹ (p ⟹ r))

Demorgan's

  @test @areequal propositional_logic_theory true (!(p || q) == (!p && !q))

Consensus theorem @testbroken @areequal propositionallogic_theory true ((x && y) || (!x && z) || (y && z)) ((x && y) || (!x && z))

end