????

prover/build

@@ -62,6 +62,7 @@ prover_smt  = prover('prover-smt',  '--main-module DRIVER-SMT  --syntax-module D
 # ----------------
 
 prover_kore.tests(inputs = glob('t/*.kore'), implicit_inputs = glob('t/definitions/*.kore'), flags = '-cCOMMANDLINE=.CommandLine')
+prover_kore.tests(inputs = glob('t/ltl/*.kore'), implicit_inputs = glob('t/definitions/*.kore'), flags = '-cCOMMANDLINE=.CommandLine')
 prover_smt .tests(inputs = glob('t/*.smt2'), flags = '-cCOMMANDLINE=.CommandLine')
 
 def log_on_success(file, message):

prover/drivers/base.md

@@ -23,7 +23,7 @@ module PROVER-CONFIGURATION
       <prover>
         <exit-code exit=""> 1 </exit-code>
         <goals>
-          <goal multiplicity="*" type="List" format="%1%i%n%2, %3%n%4%n%5n%6%n%7%n%d%8">
+          <goal multiplicity="*" type="List" format="%1%i%n%2, %3%n%4%n%5%n%6%n%7%n%d%8">
             <id format="id: %2"> .K </id>
             <parent format="parent: %2"> .K </parent>
             <k> $COMMANDLINE:CommandLine ~> $PGM:Pgm </k>

prover/drivers/kore-driver.md

@@ -68,9 +68,10 @@ in the subgoal and the claim of the named goal remains intact.
        </k>
   rule <k> claim NAME : PATTERN
            strategy STRAT
-        => subgoal(NAME, PATTERN, subgoal(PATTERN, STRAT))
+        => .K
            ...
        </k>
+       <strategy> .K => subgoal(NAME, PATTERN, STRAT) </strategy>
 ```
 
 ```k

prover/lang/kore-lang.md

@@ -159,6 +159,7 @@ only in this scenario*.
                    | "\\exists" "{" Patterns "}" Pattern        [klabel(exists)]
                    | "\\forall" "{" Patterns "}" Pattern        [klabel(forall)]
 
+                   | "\\mu" SetVariable "." Pattern             [klabel(mu)]
                      /* Sugar for \iff, \mu and application */
                    | "\\iff-lfp" "(" Pattern "," Pattern ")"    [klabel(ifflfp)]
 

prover/strategies/core.md

@@ -110,10 +110,10 @@ Proving a goal may involve proving other subgoals:
   rule <strategy> subgoal(GOAL, STRAT) => subgoal(!ID:Int, GOAL, STRAT) ... </strategy>
 
   syntax Strategy ::= "subgoal" "(" GoalId "," Pattern "," Strategy ")"
-  rule <prover>
+  rule <goals>
          ( .Bag =>
              <goal>
-               <id> ID:Int </id>
+               <id> ID </id>
                <parent> PARENT </parent>
                <strategy> SUBSTRAT </strategy>
                <k> SUBGOAL </k>
@@ -124,13 +124,13 @@ Proving a goal may involve proving other subgoals:
          )
          <goal>
            <id> PARENT </id>
-           <strategy> subgoal(ID, SUBGOAL, SUBSTRAT) => goalStrat(ID:Int) ... </strategy>
+           <strategy> subgoal(ID, SUBGOAL, SUBSTRAT) => goalStrat(ID) ... </strategy>
            <local-context> LC::Bag </local-context>
            <trace> TRACE </trace>
            ...
          </goal>
          ...
-       </prover>
+       </goals>
 ```
 
 Sometimes, we may need to combine the proofs of two subgoals to construct a proof

prover/strategies/knaster-tarski.md

@@ -19,6 +19,8 @@ for guessing an instantiation of the inductive hypothesis.
   rule getKTUnfoldables(R(ARGS), REST)
     => R(ARGS), getKTUnfoldables(REST)
     requires isUnfoldable(R)
+  rule getKTUnfoldables(\mu X . Phi, REST)
+    => \mu X . Phi, getKTUnfoldables(REST)
   rule getKTUnfoldables(S:Symbol, REST)
     => getKTUnfoldables(REST)
     requires notBool isUnfoldable(S)

prover/strategies/simplification.md

@@ -59,10 +59,19 @@ Normalize:
 
   rule <k> P::Pattern => \and(P) </k>
        <strategy> normalize ... </strategy>
-       requires \and(...) :/=K P andBool \implies(...) :/=K P
+    requires \and(...) :/=K P andBool \implies(...) :/=K P
 
   rule <k> \and(P) => \implies(\and(.Patterns), \and(P)) </k>
        <strategy> normalize ... </strategy>
+       
+  rule <k> \implies(LHS, RHS) => \implies(LHS, \and(RHS)) </k>
+       <strategy> normalize ... </strategy>
+    requires \and(...) :/=K RHS
+     andBool \exists { _ } \and(_) :/=K RHS
+
+  rule <k> \implies(LHS, RHS) => \implies(\and(LHS), RHS) </k>
+       <strategy> normalize ... </strategy>
+    requires \and(...) :/=K LHS
 
   rule <k> \implies(LHS, \and(RHS))
         => \implies(LHS, \exists { .Patterns } \and(RHS))