Quelle Proof.sml Sprache: SML

(* ========================================================================= *)
(* PROOFS IN FIRST ORDER LOGIC                                               *)
(* Copyright (c) 2001 Joe Leslie-Hurd, distributed under the BSD License     *)
(* ========================================================================= *)

structure Proof :> Proof =
struct

open Useful;

(* ------------------------------------------------------------------------- *)
(* A type of first order logic proofs.                                       *)
(* ------------------------------------------------------------------------- *)

datatype inference =
    Axiom of LiteralSet.set
  | Assume of Atom.atom
  | Subst of Subst.subst * Thm.thm
  | Resolve of Atom.atom * Thm.thm * Thm.thm
  | Refl of Term.term
  | Equality of Literal.literal * Term.path * Term.term;

type proof = (Thm.thm * inference) list;

(* ------------------------------------------------------------------------- *)
(* Printing.                                                                 *)
(* ------------------------------------------------------------------------- *)

fun inferenceType (Axiom _) = Thm.Axiom
  | inferenceType (Assume _) = Thm.Assume
  | inferenceType (Subst _) = Thm.Subst
  | inferenceType (Resolve _) = Thm.Resolve
  | inferenceType (Refl _) = Thm.Refl
  | inferenceType (Equality _) = Thm.Equality;

local
  fun ppAssume atm = Print.sequence Print.break (Atom.pp atm);

  fun ppSubst ppThm (sub,thm) =
      Print.sequence Print.break
        (Print.inconsistentBlock 1
           [Print.ppString "{",
            Print.ppOp2 " =" Print.ppString Subst.pp ("sub",sub),
            Print.ppString ",",
            Print.break,
            Print.ppOp2 " =" Print.ppString ppThm ("thm",thm),
            Print.ppString "}"]);

  fun ppResolve ppThm (res,pos,neg) =
      Print.sequence Print.break
        (Print.inconsistentBlock 1
           [Print.ppString "{",
            Print.ppOp2 " =" Print.ppString Atom.pp ("res",res),
            Print.ppString ",",
            Print.break,
            Print.ppOp2 " =" Print.ppString ppThm ("pos",pos),
            Print.ppString ",",
            Print.break,
            Print.ppOp2 " =" Print.ppString ppThm ("neg",neg),
            Print.ppString "}"]);

  fun ppRefl tm = Print.sequence Print.break (Term.pp tm);

  fun ppEquality (lit,path,res) =
      Print.sequence Print.break
        (Print.inconsistentBlock 1
           [Print.ppString "{",
            Print.ppOp2 " =" Print.ppString Literal.pp ("lit",lit),
            Print.ppString ",",
            Print.break,
            Print.ppOp2 " =" Print.ppString Term.ppPath ("path",path),
            Print.ppString ",",
            Print.break,
            Print.ppOp2 " =" Print.ppString Term.pp ("res",res),
            Print.ppString "}"]);

  fun ppInf ppAxiom ppThm inf =
      let
        val infString = Thm.inferenceTypeToString (inferenceType inf)
      in
        Print.inconsistentBlock 2
          [Print.ppString infString,
           (case inf of
              Axiom cl => ppAxiom cl
            | Assume x => ppAssume x
            | Subst x => ppSubst ppThm x
            | Resolve x => ppResolve ppThm x
            | Refl x => ppRefl x
            | Equality x => ppEquality x)]
      end;

  fun ppAxiom cl =
      Print.sequence
        Print.break
        (Print.ppMap
           LiteralSet.toList
           (Print.ppBracket "{" "}" (Print.ppOpList "," Literal.pp)) cl);
in
  val ppInference = ppInf ppAxiom Thm.pp;

  fun pp prf =
      let
        fun thmString n = "(" ^ Int.toString n ^ ")"

        val prf = enumerate prf

        fun ppThm th =
            Print.ppString
            let
              val cl = Thm.clause th

              fun pred (_,(th',_)) = LiteralSet.equal (Thm.clause th') cl
            in
              case List.find pred prf of
                NONE => "(?)"
              | SOME (n,_) => thmString n
            end

        fun ppStep (n,(th,inf)) =
            let
              val s = thmString n
            in
              Print.sequence
                (Print.consistentBlock (1 + size s)
                   [Print.ppString (s ^ " "),
                    Thm.pp th,
                    Print.breaks 2,
                    Print.ppBracket "[" "]" (ppInf (K Print.skip) ppThm) inf])
                Print.newline
            end
      in
        Print.consistentBlock 0
          [Print.ppString "START OF PROOF",
           Print.newline,
           Print.program (List.map ppStep prf),
           Print.ppString "END OF PROOF"]
      end
(*MetisDebug
      handle Error err => raise Bug ("Proof.pp: shouldn't fail:\n" ^ err);
*)

end;

val inferenceToString = Print.toString ppInference;

val toString = Print.toString pp;

(* ------------------------------------------------------------------------- *)
(* Reconstructing single inferences.                                         *)
(* ------------------------------------------------------------------------- *)

fun parents (Axiom _) = []
  | parents (Assume _) = []
  | parents (Subst (_,th)) = [th]
  | parents (Resolve (_,th,th')) = [th,th']
  | parents (Refl _) = []
  | parents (Equality _) = [];

fun inferenceToThm (Axiom cl) = Thm.axiom cl
  | inferenceToThm (Assume atm) = Thm.assume (true,atm)
  | inferenceToThm (Subst (sub,th)) = Thm.subst sub th
  | inferenceToThm (Resolve (atm,th,th')) = Thm.resolve (true,atm) th th'
  | inferenceToThm (Refl tm) = Thm.refl tm
  | inferenceToThm (Equality (lit,path,r)) = Thm.equality lit path r;

local
  fun reconstructSubst cl cl' =
      let
        fun recon [] =
            let
(*MetisTrace3
              val () = Print.trace LiteralSet.pp "reconstructSubst: cl" cl
              val () = Print.trace LiteralSet.pp "reconstructSubst: cl'" cl'
*)
            in
              raise Bug "can't reconstruct Subst rule"
            end
          | recon (([],sub) :: others) =
            if LiteralSet.equal (LiteralSet.subst sub cl) cl' then sub
            else recon others
          | recon ((lit :: lits, sub) :: others) =
            let
              fun checkLit (lit',acc) =
                  case total (Literal.match sub lit) lit' of
                    NONE => acc
                  | SOME sub => (lits,sub) :: acc
            in
              recon (LiteralSet.foldl checkLit others cl')
            end
      in
        Subst.normalize (recon [(LiteralSet.toList cl, Subst.empty)])
      end
(*MetisDebug
      handle Error err =>
        raise Bug ("Proof.recontructSubst: shouldn't fail:\n" ^ err);
*)

  fun reconstructResolvant cl1 cl2 cl =
      (if not (LiteralSet.subset cl1 cl) then
         LiteralSet.pick (LiteralSet.difference cl1 cl)
       else if not (LiteralSet.subset cl2 cl) then
         Literal.negate (LiteralSet.pick (LiteralSet.difference cl2 cl))
       else
         (* A useless resolution, but we must reconstruct it anyway *)
         let
           val cl1' = LiteralSet.negate cl1
           and cl2' = LiteralSet.negate cl2
           val lits = LiteralSet.intersectList [cl1,cl1',cl2,cl2']
         in
           if not (LiteralSet.null lits) then LiteralSet.pick lits
           else raise Bug "can't reconstruct Resolve rule"
         end)
(*MetisDebug
      handle Error err =>
        raise Bug ("Proof.recontructResolvant: shouldn't fail:\n" ^ err);
*)

  fun reconstructEquality cl =
      let
(*MetisTrace3
        val () = Print.trace LiteralSet.pp "Proof.reconstructEquality: cl" cl
*)

        fun sync s t path (f,a) (f',a') =
            if not (Name.equal f f' andalso length a = length a') then NONE
            else
              let
                val itms = enumerate (zip a a')
              in
                case List.filter (not o uncurry Term.equal o snd) itms of
                  [(i,(tm,tm'))] =>
                  let
                    val path = i :: path
                  in
                    if Term.equal tm s andalso Term.equal tm' t then
                      SOME (List.rev path)
                    else
                      case (tm,tm') of
                        (Term.Fn f_a, Term.Fn f_a') => sync s t path f_a f_a'
                      | _ => NONE
                  end
                | _ => NONE
              end

        fun recon (neq,(pol,atm),(pol',atm')) =
            if pol = pol' then NONE
            else
              let
                val (s,t) = Literal.destNeq neq

                val path =
                    if not (Term.equal s t) then sync s t [] atm atm'
                    else if not (Atom.equal atm atm') then NONE
                    else Atom.find (Term.equal s) atm
              in
                case path of
                  SOME path => SOME ((pol',atm),path,t)
                | NONE => NONE
              end

        val candidates =
            case List.partition Literal.isNeq (LiteralSet.toList cl) of
              ([l1],[l2,l3]) => [(l1,l2,l3),(l1,l3,l2)]
            | ([l1,l2],[l3]) => [(l1,l2,l3),(l1,l3,l2),(l2,l1,l3),(l2,l3,l1)]
            | ([l1],[l2]) => [(l1,l1,l2),(l1,l2,l1)]
            | _ => raise Bug "reconstructEquality: malformed"

(*MetisTrace3
        val ppCands =
            Print.ppList (Print.ppTriple Literal.pp Literal.pp Literal.pp)
        val () = Print.trace ppCands
                   "Proof.reconstructEquality: candidates" candidates
*)
      in
        case first recon candidates of
          SOME info => info
        | NONE => raise Bug "can't reconstruct Equality rule"
      end
(*MetisDebug
      handle Error err =>
        raise Bug ("Proof.recontructEquality: shouldn't fail:\n" ^ err);
*)

  fun reconstruct cl (Thm.Axiom,[]) = Axiom cl
    | reconstruct cl (Thm.Assume,[]) =
      (case LiteralSet.findl Literal.positive cl of
         SOME (_,atm) => Assume atm
       | NONE => raise Bug "malformed Assume inference")
    | reconstruct cl (Thm.Subst,[th]) =
      Subst (reconstructSubst (Thm.clause th) cl, th)
    | reconstruct cl (Thm.Resolve,[th1,th2]) =
      let
        val cl1 = Thm.clause th1
        and cl2 = Thm.clause th2
        val (pol,atm) = reconstructResolvant cl1 cl2 cl
      in
        if pol then Resolve (atm,th1,th2) else Resolve (atm,th2,th1)
      end
    | reconstruct cl (Thm.Refl,[]) =
      (case LiteralSet.findl (K true) cl of
         SOME lit => Refl (Literal.destRefl lit)
       | NONE => raise Bug "malformed Refl inference")
    | reconstruct cl (Thm.Equality,[]) = Equality (reconstructEquality cl)
    | reconstruct _ _ = raise Bug "malformed inference";
in
  fun thmToInference th =
      let
(*MetisTrace3
        val () = Print.trace Thm.pp "Proof.thmToInference: th" th
*)

        val cl = Thm.clause th

        val thmInf = Thm.inference th

(*MetisTrace3
        val ppThmInf = Print.ppPair Thm.ppInferenceType (Print.ppList Thm.pp)
        val () = Print.trace ppThmInf "Proof.thmToInference: thmInf" thmInf
*)

        val inf = reconstruct cl thmInf

(*MetisTrace3
        val () = Print.trace ppInference "Proof.thmToInference: inf" inf
*)
(*MetisDebug
        val () =
            let
              val th' = inferenceToThm inf
            in
              if LiteralSet.equal (Thm.clause th') cl then ()
              else
                raise
                  Bug
                    ("Proof.thmToInference: bad inference reconstruction:" ^
                     "\n  th = " ^ Thm.toString th ^
                     "\n  inf = " ^ inferenceToString inf ^
                     "\n  inf th = " ^ Thm.toString th')
            end
*)
      in
        inf
      end
(*MetisDebug
      handle Error err =>
        raise Bug ("Proof.thmToInference: shouldn't fail:\n" ^ err);
*)
end;

(* ------------------------------------------------------------------------- *)
(* Reconstructing whole proofs.                                              *)
(* ------------------------------------------------------------------------- *)

local
  val emptyThms : Thm.thm LiteralSetMap.map = LiteralSetMap.new ();

  fun addThms (th,ths) =
      let
        val cl = Thm.clause th
      in
        if LiteralSetMap.inDomain cl ths then ths
        else
          let
            val (_,pars) = Thm.inference th
            val ths = List.foldl addThms ths pars
          in
            if LiteralSetMap.inDomain cl ths then ths
            else LiteralSetMap.insert ths (cl,th)
          end
      end;

  fun mkThms th = addThms (th,emptyThms);

  fun addProof (th,(ths,acc)) =
      let
        val cl = Thm.clause th
      in
        case LiteralSetMap.peek ths cl of
          NONE => (ths,acc)
        | SOME th =>
          let
            val (_,pars) = Thm.inference th
            val (ths,acc) = List.foldl addProof (ths,acc) pars
            val ths = LiteralSetMap.delete ths cl
            val acc = (th, thmToInference th) :: acc
          in
            (ths,acc)
          end
      end;

  fun mkProof ths th =
      let
        val (ths,acc) = addProof (th,(ths,[]))
(*MetisTrace4
        val () = Print.trace Print.ppInt "Proof.proof: unnecessary clauses" (LiteralSetMap.size ths)
*)
      in
        List.rev acc
      end;
in
  fun proof th =
      let
(*MetisTrace3
        val () = Print.trace Thm.pp "Proof.proof: th" th
*)
        val ths = mkThms th
        val infs = mkProof ths th
(*MetisTrace3
        val () = Print.trace Print.ppInt "Proof.proof: size" (length infs)
*)
      in
        infs
      end;
end;

(* ------------------------------------------------------------------------- *)
(* Free variables.                                                           *)
(* ------------------------------------------------------------------------- *)

fun freeIn v =
    let
      fun free th_inf =
          case th_inf of
            (_, Axiom lits) => LiteralSet.freeIn v lits
          | (_, Assume atm) => Atom.freeIn v atm
          | (th, Subst _) => Thm.freeIn v th
          | (_, Resolve _) => false
          | (_, Refl tm) => Term.freeIn v tm
          | (_, Equality (lit,_,tm)) =>
            Literal.freeIn v lit orelse Term.freeIn v tm
    in
      List.exists free
    end;

val freeVars =
    let
      fun inc (th_inf,set) =
          NameSet.union set
          (case th_inf of
             (_, Axiom lits) => LiteralSet.freeVars lits
           | (_, Assume atm) => Atom.freeVars atm
           | (th, Subst _) => Thm.freeVars th
           | (_, Resolve _) => NameSet.empty
           | (_, Refl tm) => Term.freeVars tm
           | (_, Equality (lit,_,tm)) =>
             NameSet.union (Literal.freeVars lit) (Term.freeVars tm))
    in
      List.foldl inc NameSet.empty
    end;

end

quality100%

¤ Dauer der Verarbeitung: 0.15 Sekunden (vorverarbeitet) ¤

Wurzel

Suchen

Beweissystem der NASA

Beweissystem Isabelle

NIST Cobol Testsuite

Cephes Mathematical Library

Wiener Entwicklungsmethode

Haftungshinweis

Die Informationen auf dieser Webseite wurden nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit, noch Qualität der bereit gestellten Informationen zugesichert.

Bemerkung:

Die farbliche Syntaxdarstellung ist noch experimentell.