Getting started

Once you've unpacked all necessary files (see list above) you can load XRay into your Prolog-System by loading xray.pl. Here's what happens in ECLiPSe ¹:

ECRC Common Logic Programming System [sepia opium megalog parallel]
Version 3.5.2, Copyright ECRC GmbH, Wed Jan  3 12:54 1996
[eclipse 1]: [xray].
base.pl    compiled traceable 3032 bytes in 0.01 seconds
pttp.pl    compiled traceable 41276 bytes in 0.04 seconds
builtin.pl compiled traceable 6064 bytes in 0.00 seconds
model.pl   compiled traceable 18412 bytes in 0.01 seconds
io.pl      compiled traceable 7008 bytes in 0.01 seconds
db.pl      compiled traceable 840 bytes in 0.00 seconds
herbrand.pl compiled traceable 9768 bytes in 0.01 seconds
hooks_config.pl compiled traceable 0 bytes in 0.00 seconds
hooks.pl   compiled traceable 5996 bytes in 0.01 seconds
lemma_config.pl compiled traceable 1588 bytes in 0.00 seconds
lemma.pl   compiled traceable 23624 bytes in 0.04 seconds

HOOK CONFIGURATION:

body hook handling      = off
predicate hook handling = off

LEMMA CONFIGURATION:

Lemma handling = off

XRay CONFIGURATION:

delta_ordering = admissibility > compatibility .
verbose_mode = on

xray.pl compiled traceable 20404 bytes in 0.15 seconds

yes.
[eclipse 2]:

You've now loaded XRay without lemma-handling and hook-handling facilities.

Suppose you've stored your knowledge bases in a directory KB in which you've put the file adult.kb. This file can be compiled by means of the predicate xray/1 reading a file from disk and compiling it afterwards.

Here's what happens to our file adult.kb when loading it (again under ECLiPSe):

[eclipse 2]: xray('KB/adult').

XRay input formulas:
student.
adult :- student : student.
not_employed :- student : student.
not_married :- student : student.
employed :- adult : not_student.
married :- adult : not_student.
query :- married ; employed.

Classical output formulas:
[student].

Query formula:
married ; employed.
      compiled:
[married, employed].
  general combination

XRay output formulas:
student(_g996, _g998, _g1000, _g1174, _g1176, ...

 ... [here goes lots of code] ...

Compilation Phase I time: 0.2 seconds, including printing

XRay writing compiled clauses ... done.
Compilation Phase II time: 0.01 seconds, including printing

XRay compiling clauses ... adults.ckb  compiled traceable 12124 bytes in 0.03 seconds
done.
XRay compiling query ... adults.que  compiled traceable 560 bytes in 0.00 seconds
done.

Compilation Phase III time: 0.03 seconds, including printing

yes.
[eclipse 3]:

Now you can ask the initial query given in the knowledge-base using predicate query/0.

In our ECLiPSe environment, we obtain:

[eclipse 3]: query.
* model generation : [student, married]
  no unit adjunction
- satisfiability check
  no unit adjunction
  no unit adjunction
- satisfiability check
  no unit adjunction

no (more) solution.
[eclipse 4]:

In order words, our query (married ; employed) is not provable.

Let us look for a provable query and try not_married. This can be done via the predicate ask/2 taking the basename of the traeted knowledge-base and a new query and re-compiling the query by leaving the knowledge-base itself untouched:

[eclipse 4]: ask('KB/adults',not_married).
  1 unit combination

XRay output formulas:
query(_g1334, _g1338, _g1748, _g1752) :-
       model_initialization([[not_married], [student]], _g996), 
       _g1748 = [extension(1 : query)|_g1802], 
       not_married([], [], [], _g996, _g1004, _g1334, _g1338, _g1802,_g1752), 
       write_proved(_g1748, _g1752).
not_married(_g638, _g642, _g646, _g1128, _g1132, _g1502, _g1502, _g1982,_g1986) :- 
       identical_member(not_married, _g642), !, fail.
not_married(_g638, _g642, _g646, _g1228, _g1228, _g1622, _g1622, _g2122,_g2126) :- 
       identical_member(married, _g638), !, _g2122 = [reduction(married)|_g2126].

XRay writing query ... done.
XRay compiling query ... adults.que  compiled traceable 388 bytes in 0.00 seconds
done.

yes.
[eclipse 5]:

Now, we can invoke a query-answering process via query/0:

[eclipse 5]: query.
* model generation : [not_married, student]
  no unit adjunction
- satisfiability check
proved by:
 extension(1 : query)
 extension(4 : not_married)
 default(4 : (not_married :- student : [[not_married], [student]]))
 extension(4 : alpha(4, student))
 unit(1 : student)
yes.
[eclipse 6]: