jonaprieto / agda-metis Goto Github PK

View Code? Open in Web Editor NEW

1.0 1.0 1.0 783 KB

Metis Prover Reasoning for Propositional Logic in Agda

Home Page: https://jonaprieto.github.io/agda-metis/ATP.Metis.Rules.html

License: MIT License

Agda 99.68% Makefile 0.32%

agda agda-library agda-metis metis-atp theorem-proving type-theory

agda-metis's People

Contributors

Stargazers

Watchers

Forkers

asr

agda-metis's Issues

thm-reorder-v omits cases

Consider this case:

(a v b) v (c v d)

and we want and we can have

(a v d) v (b v c)

Unfortunately, thm-reorder-v doesn't prove it. Then, we need to reformulate it.

atp-conjunct

Improve the efficiency of atp-conjunct by removing the usage of this code:

conjunct-path : Prop → Prop → Path → Path
conjunct-path φ ψ path
    with ⌊ eq φ ψ ⌋
... | true  = path ∷ʳ pick
... | false
    with conj-view φ
...    | other _ = []
...    | conj φ₁ φ₂
       with conjunct-path φ₁ ψ []
...       | subpath@(_ ∷ _) = (path ∷ʳ proj₁) ++ subpath
...       | [] with conjunct-path φ₂ ψ []
...               | subpath@(_ ∷ _) = (path ∷ʳ proj₂) ++ subpath
...               | []              = []

steps-contraction is correct? I'm not sure at the moment.

In order to prove the functionality of strip function and also the atp-strip theorem,
I am seeing that the last step is to simplify the expression in the way the following does.

Γ ⊢ φ₁ ⇒ (φ₂ ⇒ φ₃)
────────────── (thm-contraction)
Γ ⊢ contraction (φ₁ ∧ φ₂ ⇒ φ₃)

contraction₀ : ℕ → Prop → Prop
contraction₀ (suc n) φ with contra-view φ
... | impl φ₁ φ₂ φ₃ = contraction₀ n ((φ₁ ∧ φ₂) ⇒ φ₃)
... | other _       = φ
contraction₀ zero φ = φ

steps-contraction : Prop → ℕ
steps-contraction φ with contra-view φ
... | impl _ _ φ₃ = 1 + steps-contraction φ₃
... | other _     = zero

thm-contraction′
  : ∀ {Γ} {φ}
  → (n : ℕ)
  → Γ ⊢ φ
  → Γ ⊢ contraction₀ n φ

contraction : Prop → Prop
contraction φ = contraction₀ (steps-contraction φ) φ

thm-contraction
  : ∀ {Γ} {φ}
  → Γ ⊢ φ
  → Γ ⊢ contraction φ
thm-contraction {Γ} {φ} Γ⊢φ = thm-contraction′ (steps-contraction φ) Γ⊢φ

I am not sure about steps-contraction φ, if it is counting well the number of calls we should call to contraction₀ function.

clausify evidence

The following confirms that clausify performs CNF conversion.

Excerpt from source:

        | NONE =>
          let
            val simp = simplifyAdd simp th

            val fm = basicCnf fm

            val inf = Clausify th
          in

Normalized Formula data type

Starting with the definition (Normalize .sig and Normalize.sml).

datatype formula =
    True
  | False
  | Literal of (NameSet.set , Literal.literal)
  | And     of (NameSet.set , count , formula Set.set)
  | Or      of (NameSet.set , count , formula Set.set)
  | Xor     of (NameSet.set , count , bool , formula Set.set)
  | Exists  of (NameSet.set , count , NameSet.set , formula)
  | Forall  of (NameSet.set , count , NameSet.set , formula;)

How we must compare them:

fun compare f1_f2 =
    if Portable.pointerEqual f1_f2 then EQUAL
    else
      case f1_f2 of

        (True,True) => EQUAL
      | (True,_) => LESS
      | (_,True) => GREATER

      | (False,False) => EQUAL
      | (False,_) => LESS
      | (_,False) => GREATER

      | (Literal (_,l1), Literal (_,l2)) => Literal.compare (l1,l2)
      | (Literal _, _) => LESS
      | (_, Literal _) => GREATER

      | (And (_,_,s1), And (_,_,s2)) => Set.compare (s1,s2)
      | (And _, _) => LESS
      | (_, And _) => GREATER

      | (Or (_,_,s1), Or (_,_,s2)) => Set.compare (s1,s2)
      | (Or _, _) => LESS
      | (_, Or _) => GREATER

      | (Xor (_,_,p1,s1), Xor (_,_,p2,s2)) =>
        (case boolCompare (p1,p2) of
           LESS => LESS
         | EQUAL => Set.compare (s1,s2)
         | GREATER => GREATER)
      | (Xor _, _) => LESS
      | (_, Xor _) => GREATER

The conversion between the two data types:

fun fromFormula fm =
    case fm of
        Formula.True      => True
      | Formula.False     => False
      | Formula.Atom atm  => Literal (Atom.freeVars atm, (true,atm))
      | Formula.Not p     => negateFromFormula p
      | Formula.And (p,q) => And2 (fromFormula p, fromFormula q)
      | Formula.Or (p,q)  => Or2 (fromFormula p, fromFormula q)
      | Formula.Imp (p,q) => Or2 (negateFromFormula p, fromFormula q)
      | Formula.Iff (p,q) => Xor2 (negateFromFormula p, fromFormula q)

and negateFromFormula fm =
    case fm of
        Formula.True      => False
      | Formula.False     => True
      | Formula.Atom atm  => Literal (Atom.freeVars atm, (false,atm))
      | Formula.Not p     => fromFormula p
      | Formula.And (p,q) => Or2 (negateFromFormula p, negateFromFormula q)
      | Formula.Or (p,q)  => And2 (negateFromFormula p, negateFromFormula q)
      | Formula.Imp (p,q) => And2 (fromFormula p, negateFromFormula q)
      | Formula.Iff (p,q) => Xor2 (fromFormula p, fromFormula q)

Missing case in atp-conjunct, fails projecting.

Because of,

conjunct : Prop → Prop → Prop
conjunct x ω with c-view x ω
conjunct .(φ ∧ ψ) ω | conj φ ψ .ω
  with ⌊ eq φ ω ⌋ | ⌊ eq ψ ω ⌋
...  | true  | _     = φ
...  | false | true  = ψ
...  | false | false = conjunct φ ω
conjunct x ω | other .x .ω = x

Using the problem impl-4.agda generated by Athena with its test problems:

subgoal₀ : Prop
subgoal₀ = ((p ∧ (p ⇒ q)) ⇒ q)

t : Γ , ¬ subgoal₀ ⊢ ¬ q ∧ (p ∧ ((¬ p) ∨ q))
t = thm-cnf (atp-strip (assume {Γ = Γ} (atp-negate subgoal₀)))

c1 : Γ , ¬ subgoal₀ ⊢ ¬ q
c1 = atp-conjunct (¬ q) t

c2 : Γ , ¬ subgoal₀ ⊢ (¬ p) ∨ q
c2 = atp-conjunct {!¬ p ∨ q!} t

The hole in c2 can not refine. But, it should be.

Splitting goals: proving atp-split

Splitting a Goal

Based on Metis' source code, I believe strip inference rule is performing
the following transformations (sketch) at each iteration per each conjunct that it produces.

        Γ ⊢ ⊤
      ────────
        Γ ⊢ ⊤

        Γ ⊢ φ₁ ∧ φ₂
      ────────────
        Γ ⊢ φ₁  and  Γ , φ₁  ⊢ φ₂

        Γ ⊢ φ₁ ∨ φ₂
      ────────────
        Γ, ¬ φ₁ ⊢ φ₂

        Γ ⊢ φ₁ ⇒ φ₂
      ────────────
        Γ, φ₁ ⊢ φ₂

         Γ ⊢ φ₁ ⇔ φ₂
      ────────────
        Γ, φ₁ ⊢ φ₂  and  Γ, φ₂ ⊢ φ₁

        Γ ⊢ ¬ (¬ φ)
      ────────────────
        Γ ⊢ φ

        Γ ⊢ ¬ (φ₁ ∧ φ₂)
      ──────────────────
        Γ , φ₁ ⊢ ¬ φ₂

        Γ ⊢ ¬ (φ₁ ∨ φ₂)
      ─────────────────
       Γ ⊢ ¬ φ₁  and  Γ , ¬ φ₁ ⊢ ¬ φ₂

        Γ ⊢ ¬ (φ₁ ⇒ φ₂)
      ───────────────────
        Γ ⊢ φ₁   and Γ ,  φ₁ ⊢ ¬ φ₂

       Γ ⊢ ¬ (φ₁ ⇔ φ₂)
      ────────────
        Γ, φ₁ ⊢ ¬ φ₂  and  Γ, ¬ φ₂ ⊢ φ₁

Improve the proof for build-∨

build-∨ : Prop → Prop → Prop
build-∨ φ ψ
  with ⌊ eq φ ψ ⌋
... | true  = ψ
... | false
    with disj-view ψ
...    | other _    = φ
...    | disj ψ₁ ψ₂
       with ⌊ eq (build-∨ φ ψ₁) ψ₁ ⌋
...       | true = (build-∨ φ ψ₁) ∨ ψ₂ -- TODO : return ψ₁ and use subst theorem.
...       | false
          with ⌊ eq (build-∨ φ ψ₂) ψ₂ ⌋
...          | true  = ψ₁ ∨ (build-∨ φ ψ₂)  -- TODO: return ψ₂ and use subst theorem.
...          | false = φ

atp-resolve exhibits a pattern

Based on many TSTP derivations from the pro-pack, I have two guesses.

The inference has two arguments, the literal and the list of two derivations to apply the resolution theorem,
In such a list, the positive literal appears in the first one formula whereas the negation of the literal appears in the second formula.

Then, we likely say that resolve rule behaves exactly as the Metis' logical kernel says.

   L \/ C    ~L \/ D                                                
 --------------------- resolve L                                     
      C \/ D                                                            
                                                                 
 The literal L must occur in the first theorem, and the literal ~L must 
 occur in the second theorem.

Deduce $false in this case

In impl-2.tstp problem, canonicalize is not concluding $false.

Consider this new case.

canonicalize (¬ ((p ∧ q) ⇒ p)) ⊥

One of the problems trying to justify clausify and canonicalize is the ordering of the subformulas
after applying one of these inferences rules. Since we recently added support for reordering a conjunction and a disjunction. We want that the next step supports a mix of those cases.

Here a problem sample.

Original:
p ∨ (q ∨ (r ∧ (s ∨ t)))

One of many reordering:
((t ∨ s) ∧ r) ∨ p) ∨ q

canonicalize

Canonicalize inference normalizes the formula using nnf and other procedures.
I found support for the nnf theorem in agda-prop that coincides with the nnf of metis prover in Normalize.sml:

fun fromFormula fm =
    case fm of
      Formula.True => True
    | Formula.False => False
    | Formula.Atom atm => Literal (Atom.freeVars atm, (true,atm))
    | Formula.Not p => negateFromFormula p
    | Formula.And (p,q) => And2 (fromFormula p, fromFormula q)
    | Formula.Or (p,q) => Or2 (fromFormula p, fromFormula q)
    | Formula.Imp (p,q) => Or2 (negateFromFormula p, fromFormula q)
    | Formula.Iff (p,q) => Xor2 (negateFromFormula p, fromFormula q)
    | Formula.Forall (v,p) => Forall1 (v, fromFormula p)
    | Formula.Exists (v,p) => Exists1 (v, fromFormula p)

and negateFromFormula fm =
    case fm of
      Formula.True => False
    | Formula.False => True
    | Formula.Atom atm => Literal (Atom.freeVars atm, (false,atm))
    | Formula.Not p => fromFormula p
    | Formula.And (p,q) => Or2 (negateFromFormula p, negateFromFormula q)
    | Formula.Or (p,q) => And2 (negateFromFormula p, negateFromFormula q)
    | Formula.Imp (p,q) => And2 (fromFormula p, negateFromFormula q)
    | Formula.Iff (p,q) => Xor2 (fromFormula p, fromFormula q)
    | Formula.Forall (v,p) => Exists1 (v, negateFromFormula p)
    | Formula.Exists (v,p) => Forall1 (v, negateFromFormula p);

And we have from agda-prop:

nnf′ : ℕ → Prop → Prop
nnf′ (suc n) φ
  with n-view φ
...  | conj φ₁ φ₂   = nnf′ n φ₁ ∧ nnf′ n φ₂
...  | disj φ₁ φ₂   = nnf′ n φ₁ ∨ nnf′ n φ₂
...  | impl φ₁ φ₂   = nnf′ n ((¬ φ₁) ∨ φ₂)
...  | biimpl φ₁ φ₂ = nnf′ n ((φ₁ ⇒ φ₂) ∧ (φ₂ ⇒ φ₁))
...  | nconj φ₁ φ₂  = nnf′ n ((¬ φ₁) ∨ (¬ φ₂))
...  | ndisj φ₁ φ₂  = nnf′ n ((¬ φ₁) ∧ (¬ φ₂))
...  | nneg φ₁      = nnf′ n φ₁
...  | ntop         = ⊥
...  | nbot         = ⊤
...  | nimpl φ₁ φ₂  = nnf′ n (¬ (φ₂ ∨ (¬ φ₁)))
...  | nbiim φ₁ φ₂  = nnf′ n (¬ ((φ₁ ⇒ φ₂) ∧ (φ₂ ⇒ φ₁)))
...  | other .φ     = φ
nnf′ zero φ         = φ

Two cases differs a little, the negation of an implication and the negation of a biconditional. Nevertheless, the first case is only a step-behind of the metis version.

Missing proofs for auxiliar theorem in Resolve module

Remove this postulate.

postulate
  thm-helper-resolve
    : ∀ {Γ} {φ}
    → Γ ⊢ φ
    → Γ ⊢ helper-resolve φ

Theorems to simplify expressions

Simplify, canonicalize and clausify are inference rules that at some point apply different theorems to simplify the expression. This intends to be that list.

All formulas are in their NNF form.