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, eclasslimit = 5000)
  params = SaturationParams(
    timeout = timeout,
    eclasslimit = eclasslimit,

scheduler=Schedulers.ScoredScheduler, schedulerparams=(1000,5, Schedulers.exprsize))

    scheduler = Schedulers.BackoffScheduler,
    schedulerparams = (6000, 5),
  )

  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

This page was generated using Literate.jl.