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 books, live events, courses curated by job role, and more from O’Reilly and nearly 200 top publishers.