Home

prolog2pml.pl is a Prolog program that dumps clause trees as Proof Markup Language (PML 2) justifications.

Using prolog2pml.pl to understand why nick is a cool person ;-)

This wiki describes how to use prolog2pml.pl in the context of a very simple Prolog program that determines whether people are considered cool. It assumes you have access to a command prompt on your machine.

Step 1. Requirements

• Clone swi-prolog

% git clone git://www.swi-prolog.org/home/pl/git/pl-devel.git
% cd pl-devel
% ./prepare

• Install swi-prolog

% cd src
% ./configure
% gmake
% gmake check
% gmake install

• If you want precompiled executable installers or have problems with building swi-prolog, please visit http://www.swi-prolog.org/download/stable

• Clone the prolog2pml repository:

% git clone https://github.com/nicholasdelrio/prolog2pml.git

Step 2. Inspect the prolog test file isCool.pl

• Under the prolog2pml base repo, navigate inside the programs directory and notice some sample Prolog programs for you to play with:

  • isCool.pl: the program this tutorial is based on
  • threat-detection.pl: program to determine if a cargo truck should be considered dangerous
  • threat-detection-simplified.pl: a simpler version of threat-detection.pl
  • visko.pl: a program to test whether a format can be converted into another format

• Let us focus on isCool.pl, shown below:

%--- Asserted Facts by someone other than Nick ;-)
isWellKnown(nick).
isWellLiked(nick).
isComputerScientist(nick).

%--- Popularity Rules
isPopular(X) :- isWellKnown(X), isWellLiked(X).
isCool(X) :- isPopular(X); isComputerScientist(X).

• The first segment of code asserts some facts about a person named nick (No I did not assert these statements myself :-)
• The second segment defines some rules for determining if a person X is cool. The rules read as follows:

Someone X is popular if s/he is well known and well liked.
Someone X is cool if s/he is popular OR is a computer scientist.

Step3. Loading Prolog Programs prolog2pml.pl and isCool.pl

• Using a command prompt, navigate to the root of your prolog2pml repository

• Invoke SWI-Prolog and load both prolog2pml.pl and isCool.pl:

  • % swipl
  • consult('prolog2pml').
  • consult('isCool').

C:\Users\Public\git\prolog2pml>swipl
Welcome to SWI-Prolog (Multi-threaded, 64 bits, Version 5.10.5)
Copyright (c) 1990-2011 University of Amsterdam, VU Amsterdam
SWI-Prolog comes with ABSOLUTELY NO WARRANTY. This is free software,
and you are welcome to redistribute it under certain conditions.
Please visit http://www.swi-prolog.org for details.

For help, use ?- help(Topic). or ?- apropos(Word).

1 ?- consult('prolog2pml').
% prolog2pml compiled 0.02 sec, 31,744 bytes
true.

2 ?- consult('./programs/isCool.pl').
% ./programs/isCool.pl compiled 0.00 sec, 2,376 bytes
true.

Step 4. Running isCool.pl

• Lets query the loaded Prolog knowledge base and see what people are cool. You simply type in the name of the predicate and provide a binding for the predicate variable, e.g., isCool(brad-pitt).
• REMEMBER TO INCLUDE A PERIOD AT THE END OF THE QUERY:

3 ?- isCool(brad-pitt).
false.

4 ?- isCool(nick).
true .

• So we see that since our knowledge base knows only about nick, brad-pitt is not a cool person, but nick is LOL!

Step 5. Generating a PML Justification

• A suspicious person, e.g., a person who does not like nick, might want to know why the system concluded that nick is cool.
• The why(+Clause, ?URI) predicate can be used to dump a PML trace that justifies why someone is cool, or why any statement is true for that matter. For example:

5 ?- why(isCool(nick),URI).
Generating proof tree file at ./pml/pml-proof.owl
URI = "https://raw.github.com/nicholasdelrio/prolog2pml/master/pml/pml-proof.owl#pml-proof_1".

• LIMITATION: currently, prolog2pml can only explain TRUE statements and does not provide justifications for false statements. Thus, we cannot currently dump PML explaining why brad-pitt is not popular
• By entering why(isCool(nick),URI)., prolog2pml.pl generated a PML proof justifying why isCool(nick) is true and bound the URI of justification to the variable URI.
• If we look in the directory pml, you will see a file named pml-proof.owl that contains the PML justifying why nick is cool.
• In Prolog, + means that you must supply a value for this variable, in this case a clause, e.g., isCool(nick).
• The ? specifies that the adjacent variable is an "out" variable, and that Prolog will bind a value for you, in this case, a URI.

Step 6. Controlling the URI and Dump location of the PML Justifications

As you can see from the output of running prolog2pml.pl, there are some preconfigured settings controlling what URI is associated with the PML justifications as well as where on the file system the justifications get dumped.

Generating proof tree file at ./pml/pml-proof.owl
URI = "https://raw.github.com/nicholasdelrio/prolog2pml/master/pml/pml-proof.owl#pml-proof_1".

You can change both the URI and dump locations of the justifications by editing prolog2pml.pl. Near the top of the file you will find:

hasProofName('pml-proof').
hasDumpDir('./pml/').
hasBaseURL('https://raw.github.com/nicholasdelrio/prolog2pml/master/pml/').

• hasProofName: sets the name of the file the PML justification resides in
• hasDumpDir: sets the directory where the justification will be written to
• hasBaseURL: sets the base URL that the justification's URI will be minted from

Step 7. Understanding the Dumped PML