12.7. Proofs

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", ...

Get Building Parsers with Java™ now with the O’Reilly learning platform.

O’Reilly members experience live online training, plus books, videos, and digital content from nearly 200 publishers.