INSTANTIATE 0.1 -- a logic instantiator Instantiate takes as its input a logical formula with variables and produces a ground formula that is equivalent to the the input formula. Its main application domain is intended to be instantiating propositional translations of the planning problem. As a program, instantiate is a quick hack based on lparse-1.0.13 source code. In particular this means that even when propositional schemata are instantiated, there is the stable model semantics of cardinality constraint logic programs hidden underneath. This may cause a surprising behavior occasionally. Instantiate offers few syntactic extensions that are intended to make it easier to write propositional implications (as well as a syntactic limitation that cardinality constraints may not occur in rule bodies. This may be removed in a future version). The intended syntax for input looks something like this: #option --true-negation --totalize-negations --dlp #state at(_, _, _). #action move(_, _, _, _). #type vacuum(V). #type next_to(F, T). #type time(I). time( 1 .. t ). move(V, F, T, I) -> at(V, F, I). move(V, F, T, I) -> at(V, T, I+1). -at(V, Y, I), location(Y), at(V, Y, I+1) -> { move(V, X, Y, I) : next_to(X, Y) }. L_1 != L_2 -> -at(V, L_1, I) | -at(V, L_2, I). Next we'll go through the program one line at a time to see their meanings: #option --true-negation --totalize-negations --dlp Defines the instantiate command line options. All three are original lparse options and their semantics is: --true-negation: interpret a literal -a(1) to be the classical negation of the atom a(1). --totalize-negations: add a clause { a(1), -a(1) } to the for every negative literal -a(1) that occurs in the program. Note that this is not necessary in every case, but leaving it out may lead to strange behavior occasionally, especially when the output of instantiate is fed directly to 'gnt2'. --dlp: put the output into format that 'gnt2' and 'dimacs' understand. Next, #state at(_, _, _). #action move(_, _, _, _). defines the predicate at/3 to encode facts about the state of the universe, while move/4 is an action that operates with the state. (The definitions are not actually used for much, mainly they ensure that rules depending on them are not accidentally dropped from the instantiation in the case of simple program encodings). The next lines of the program are type definitions for variables. For example: #type time(I). #type next_to(F, T). define that the variable 'I' has the type time/1 in each place of the program while 'F' and 'T' have a 2-ary type next_to/2. Instantiate demands that every variable that occurs in a rule has to get its type from somewhere. There are two basic possbilities for the source. Either a #type declaration or else the body of the rule has to contain a type predicate for it. The next line: time( 1 .. t ). defines the type predicate time/1 to be true for all integers from 1 upto t where t is given as a command line argument of instantiate using the '-c t = X' syntax. The actual logical sentences are given either as logic programming rules or implications of the form: move(V, F, T, I) -> at(V, F, I). As implications are internally translated into rules, the same things apply for both of them. A rule has the head (at(V, F, I) in the case above), and the body (move(V, F, T, I)). The rules are disjunctive, meaning that you may have more than one atom in the head. For example, L_1 != L_2 -> -at(V, L_1, I) | -at(V, L_2, I). states that if L_1 does not equal to L_2, then either -at(V, L_1, I) or -at(V, L_2,I) has to be true. There's a number of built-in predicates and functions to handle stuff like the basic arithmetic operations and equality testing. See lparse manual for details. Finally ,a rule of the form: -at(V, Y, I), location(Y), at(V, Y, I+1) -> { move(V, X, Y, I) : next_to(X, Y) }. implements existential quantification. Basically it is saying that if all three atoms in the body are true (where 'location(Y)' is a type predicate giving the type for the variable 'Y'), then there some X and Y (where next_to(X, Y) is true, that is the type for the pair is next_to/2) for which move(V, X, Y, I) is true. A FEW WARNINGS FOR USERS! 1. Don't use a #type declaration for variables that you wish to existentially quantify (i.e., when you use the a(X) : b(X) notation). Do it like in the rule above, with taking new variables and using type predicates in the rule bodies. Otherwise you'll probably silently transform the variables into universal ones. [This is a questionable feature of lparse that will get fixed some day.] 2. The base code is for instantiating according stable model semantics. This means that sometimes rules may be left out from the output if they can't ever be applied under the stable semantics. For example, if you have a rule a(X) -> b(X) but do not mention a(X) anywhere else in the program, then all such rules are silently dropped from the output. There are two ways around this: (a) Use #state, #action, or #nondomain declarations for a/1. (b) Use the command line option '-d all'. 3. If you instantiate the program with the command line option '-t', you will get out a number of logic program rules. It may take some time to get used to the syntax if you are not accustomed to it before. 4. The lparse semantics for --true-negation is three valued. If is possible that neither 'a' nor '-a' is true in a model if --totalize-negations is not used. 5. A feature related to the 2nd point is that if you have rules of the form: a(X), b(X) -> c(X). where neither a(X) nor b(X) has a recursive definition, then instantiate generates only those rule instances for which both a(X) and b(X) are always true, and no others. In most cases this is the desired behavior but it may cause strange behavior if the user doesn't expect it.