| The engine proves a query by unifying the query's structures with facts in a program. Queries can contain a series of structures, each of which must be true for the query to succeed. When a query has multiple structures, its first structure unifies with some axiom in the program, which typically establishes values for some of the query's variables . The remaining structures attempt to establish their truth with these variable values in place. Consider a collection of facts about construction companies and a supplier's fees (in drachmas) for delivery to their locations: charge(athens, 23); charge(sparta, 13); charge(milos, 17); customer("Marathon Marble", sparta); customer("Acropolis Construction", athens); customer("Agora Imports", sparta); To see the shipping charge for each customer, you can create a query from two structures so that the query would print itself as charge(City, Fee), customer(Name, City) A variable's scope is the query in which it appears. In this query the variable City is the same variable in both structures. As a result, the query joins on the City variable. When the query first proves itself, it unifies its charge structure with the first charge fact in the program. This unification causes the City variable to unify with athens . The query continues its proof, trying to prove customer(Name, athens) This structure succeeds when it unifies with customer("Acropolis Construction", athens); When the query's last structure succeeds, the proof succeeds. At this point, you could print the query's variables to see the values they unified with during the proof: City: athens Fee: 23 Name: Acropolis Construction Here is a program that loads the shipping facts and queries them: package sjm.examples.engine; import sjm.engine.*; /** * Show a simple query proving itself. */ public class ShowProof { /** * Return a small database of shipping charges. */ public static Program charges() { Fact [] facts = new Fact[]{ new Fact("charge", "athens", new Integer(23)), new Fact("charge", "sparta", new Integer(13)), new Fact("charge", "milos", new Integer(17)) }; return new Program(facts); } /** * Return a small database of customers. */ public static Program customers() { Fact [] facts = new Fact[]{ new Fact("customer", "Marathon Marble", "sparta"), new Fact("customer", "Acropolis Construction", "athens"), new Fact("customer", "Agora Imports", "sparta") }; return new Program(facts); } /** * Show a simple query proving itself. */ public static void main(String[] args) { Program p = new Program(); p.append(charges()); p.append(customers()); System.out.println("Program:"); System.out.println(p); Variable city = new Variable("City"); Variable fee = new Variable("Fee"); Variable name = new Variable("Name"); Structure s1 = new Structure( "charge", new Term[] {city, fee}); Structure s2 = new Structure( "customer", new Term[] {name, city}); // charge(City, Fee), customer(Name, City) Query q = new Query(p, new Structure[] {s1, s2}); System.out.println("\nQuery:"); System.out.println(q); System.out.println("\nProofs:"); while (q.canFindNextProof()) { System.out.println("City: " + city); System.out.println("Fee: " + fee); System.out.println("Name: " + name); System.out.println(); } } } This class has static methods that create Program objects that contain facts about charges and customers. The main() method creates one Program object as a collection of all these facts, constructs a query, and proves it repeatedly. Running this program prints the following: Program: charge(athens, 23); charge(sparta, 13); charge(milos, 17); customer(Marathon Marble, sparta); customer(Acropolis Construction, athens); customer(Agora Imports, sparta); Query: charge(City, Fee), customer(Name, City) Proofs: City: athens Fee: 23 Name: Acropolis Construction City: sparta Fee: 13 Name: Marathon Marble City: sparta Fee: 13 Name: Agora Imports The first proof results from proving the charge structure and then the customer structure. The remaining proofs depend on the engine's ability to backtrack. 12.7.1 Backtracking The power of a logic engine lies in its ability to find multiple proofs. After a query finds one proof, you can ask it to find another. The query relays this request to its last structure. In the shipping company example, the first proof of the query finds City: athens Fee: 23 Name: Acropolis Construction If you ask the query for another proof, the query asks its last structure for another proof. When a structure seeks a new proof, it unbinds any variables it bound in proving itself previously. In this case, the last structure of the query unbinds the Name variable. Thus, the query's last structure searches for a new proof of customer(Name, athens) The City variable remains bound to athens because the last structure neither bound nor unbound that variable in its proof. Because there is no other customer in Athens, this structure's proof fails. The query does not give up but rather backtracks, or asks the preceding structure for a new proof. In this example, the query backtracks to its charge structure. This structure unbinds its City variable and finds the next axiom it can unify with: charge(sparta, 13) Because this structure succeeds, the query starts proving forward again. Now the query asks the structure customer(Name, sparta) for a proof, which succeeds by unifying with customer("Marathon Marble", sparta) Because this succeeds, the query succeeds and you can again print the query's variables: City: sparta Fee: 13 Name: Marathon Marble Now if you ask the query for another proof, the query again asks its last structure for a new proof. This time the structure succeeds by finding a new proof for customer(Name, sparta) This structure unifies with customer("Agora Imports", sparta) The query succeeds and the program prints City: sparta Fee: 13 Name: Agora Imports Pressing on, you ask the query for another proof. There are no more customers in Sparta, so the last structure fails. The query's first structure finds that you know the fee for shipping to Milos, and the query tries to prove forward. There are no customers in Milos at present, and so the customer structure in the query fails. The query backtracks to its charge structure, looking for a new proof. There are no other charge axioms to unify with, so the first structure of the query fails, and the entire query fails. To summarize, a query proves itself by proving each structure in turn . When a structure fails to find a proof, the query backtracks to a preceding structure to look for a new proof. If this fails, the query backtracks again until the first structure fails and the entire proof fails. If, after backtracking, a query finds a proof of a structure, this structure usually binds new values for some of the query's variables. This means that there are new chances for the later structures to find new proofs. The proof again moves forward, trying to prove each of the following structures. A query backtracks and proves forward until it proves all its structures or until all its structures fail. Rules prove themselves in the almost same way that queries do. A structure can prove itself by unifying with a rule and asking the tail of the rule to prove itself. The tail is a series of structures that proves itself exactly the way a query would. | 
