diff --git a/prover/drivers/base.md b/prover/drivers/base.md index 3c26ac868..415e8c9e9 100644 --- a/prover/drivers/base.md +++ b/prover/drivers/base.md @@ -1,13 +1,13 @@ Configuration ============= -The configuration consists of a assoc-commutative bag of goals. Only goals -marked `` are executed to control the non-determinism in the system. The -`` cell contains the Matching Logic Pattern for which we are searching for a -proof. The `` cell contains an imperative language that controls which -(high-level) proof rules are used to complete the goal. The `` cell -stores a log of the strategies used in the search of a proof and other debug -information. Eventually, this could be used for constructing a proof object. +The configuration consists of a list of goals. The first goal is considered +active. The `` cell contains the Matching Logic Pattern for which we are +searching for a proof. The `` cell contains an imperative language +that controls which (high-level) proof rules are used to complete the goal. The +`` cell stores a log of the strategies used in the search of a proof and +other debug information. Eventually, this could be used for constructing a proof +object. ```k module PROVER-CONFIGURATION @@ -23,8 +23,7 @@ module PROVER-CONFIGURATION 1 - - true:Bool + .K .K $COMMANDLINE:CommandLine ~> $PGM:Pgm diff --git a/prover/strategies/core.md b/prover/strategies/core.md index d22c677e9..54de8a0ad 100644 --- a/prover/strategies/core.md +++ b/prover/strategies/core.md @@ -89,18 +89,16 @@ completed, its result is replaced in the parent goal and the subgoal is removed. ```k syntax Strategy ::= goalStrat(GoalId) rule - PID - _ => true - goalStrat(ID) => RStrat ... - ... - ( ID - true:Bool PID RStrat:TerminalStrategy ... => .Bag ) + PID + goalStrat(ID) => RStrat ... + ... + ... ``` @@ -116,7 +114,6 @@ Proving a goal may involve proving other subgoals: ( .Bag => ID:Int - true PARENT SUBSTRAT SUBGOAL @@ -127,7 +124,6 @@ Proving a goal may involve proving other subgoals: ) PARENT - true => false subgoal(ID, SUBGOAL, SUBSTRAT) => goalStrat(ID:Int) ... LC::Bag TRACE