We will now discuss each of these two steps in some detail.
Describing a transition system by a set of clauses. Take, for instance, transition system TS1 from Section 0.1. If we create a file containing the CCalc description of this system given in Section 1.1 and loadf that file, then we'll able to display the clauses produced by CCalc using the command
| ?- show_clauses.(Try it!) We'll see 3 clauses on the screen:
-(0:a) ++ 1:p. -(1:p) ++ 0:p ++ 0:a. -(0:p) ++ 1:p.(In the language of CCalc, - is negation and ++ is disjunction.) The assignments of truth values to the atoms 0:p, 0:a and 1:p that satisfy these clauses exactly correspond to the edges of the given transition system. For instance, mapping 0:p to f and 1:p, 0:a to t corresponds to the horizontal edge from p=f to p=t labeled a=t.
The clauses formed by CCalc are propositional, that is to say, their atoms do not contain variables. The variables occurring in schematic propositions, such as I in file coins, are eliminated by grounding -- substituting all possible values for each variable -- prior to turning propositions into clauses.
Generating the clauses is accomplished by translating propositions into causal rules and completing the rules, as described in Section 2 of NMCT, and then clausifying the completion. Information on the number of causal rules that have been produced is displayed by CCalc in response to the loadf command, along with the number of atoms occurring in the rules and the number of clauses obtained after completion and clausification:
% 3 atoms, 7 rules, 3 clausesThe rules themselves can be displayed using the command
| ?- show_rules.Turning a query into a set of clauses. Once the value of maxstep is specified, CCalc generates a set of clauses representing the paths of length maxstep. In the example above, if the value of maxstep in the query is 3, this set will consist of the clauses produced earlier
-(0:a) ++ 1:p. -(1:p) ++ 0:p ++ 0:a. -(0:p) ++ 1:p.and two "copies" of these clauses, with the "time stamps" 0, 1 incremented first by 1 and then by 2:
-(1:a) ++ 2:p. -(2:p) ++ 1:p ++ 1:a. -(1:p) ++ 2:p. -(2:a) ++ 3:p. -(3:p) ++ 2:p ++ 2:a. -(2:p) ++ 3:p.The assignments of truth values to atoms that satisfy all 9 clauses are in a 1-1 correspondence with the paths of length 3 in the given transition system. The process of forming copies of the initially generated clauses by incrementing time stamps is called shifting.
When the shifting process is completed, the resulting set of clauses is extended by the conditions on the path that are included in the query, such as assumptions about the initial values of fluents in a prediction problem. The assignments of truth values to atoms that satisfy the extended set of clauses represent the answers to the query. This extended set is passed to a SAT solver to find an answer.
Forward to Section 1.5: Setting Parameters Back to Section 1.3: Running CCalc Up to the Table of Contents