*****************************************************************************
 *                                                                           *
 *           ILLUSTRATION OF FORMULA MANIPULATION USING TEYJUS               *
 *                                                                           *
 *  The script that follows shows the compilation and execution of the code  *
 *  for checking if a given formula satisfies the required constraints of    *
 *  a goal formula or a definite clause in Horn clause logic.                *
 *                                                                           *
 *****************************************************************************

(gopalan@Diligence 49)% teyjus -p examples/handbook/logic 
Welcome to Teyjus

Copyright (C) 1999 Gopalan Nadathur
Teyjus comes with ABSOLUTELY NO WARRANTY
This is free software, and you are welcome to redistribute it
under certain conditions.  Please view the accompanying file
"COPYING" for more information.
Teyjus> #compile hcsyntax_examples.
Reading module signature from file examples/handbook/logic/hcsyntax_examples.sig
Accumulating signature logic_types from file examples/handbook/logic/logic_types.sig
Accumulating signature logic_basic from file examples/handbook/logic/logic_basic.sig
Accumulating signature logic_types from file examples/handbook/logic/logic_types.sig
Accumulating signature logic_vocab from file examples/handbook/logic/logic_vocab.sig
Accumulating signature logic_types from file examples/handbook/logic/logic_types.sig
Signature of module hcsyntax_examples successfully processed
Obtaining source for module hcsyntax_examples from file examples/handbook/logic/hcsyntax_examples.mod

Processing declarations in source for module hcsyntax_examples

Attempting to accumulate module hc_syntax
Reading module signature from file examples/handbook/logic/hc_syntax.sig
Accumulating signature logic_types from file examples/handbook/logic/logic_types.sig
Accumulating signature logic_basic from file examples/handbook/logic/logic_basic.sig
Accumulating signature logic_types from file examples/handbook/logic/logic_types.sig
Signature of module hc_syntax successfully processed
Obtaining source for module hc_syntax from file examples/handbook/logic/hc_syntax.mod
Accumulated module hc_syntax successfully processed

Attempting to accumulate module refl_syntax
Reading module signature from file examples/handbook/logic/refl_syntax.sig
Accumulating signature logic_types from file examples/handbook/logic/logic_types.sig
Accumulating signature logic_basic from file examples/handbook/logic/logic_basic.sig
Accumulating signature logic_types from file examples/handbook/logic/logic_types.sig
Accumulating signature logic_vocab from file examples/handbook/logic/logic_vocab.sig
Accumulating signature logic_types from file examples/handbook/logic/logic_types.sig
Signature of module refl_syntax successfully processed
Obtaining source for module refl_syntax from file examples/handbook/logic/refl_syntax.mod

Accumulating signature logic_types from file examples/handbook/logic/logic_types.sig

Accumulating signature logic_basic from file examples/handbook/logic/logic_basic.sig
Accumulating signature logic_types from file examples/handbook/logic/logic_types.sig

Accumulating signature logic_vocab from file examples/handbook/logic/logic_vocab.sig
Accumulating signature logic_types from file examples/handbook/logic/logic_types.sig

Processing declarations in source for module refl_syntax

Accumulated module refl_syntax successfully processed

Checking compatibility of accumulates and imports into module hcsyntax_examples
No (outward) compatibility errors found

Writing bytecode to file examples/handbook/logic/hcsyntax_examples.lp
Teyjus> #load hcsyntax_examples.
Teyjus> #query hcsyntax_examples.

[hcsyntax_examples] ?- test_goal 1.

yes

[hcsyntax_examples] ?- test_goal 2.

no (more) solutions

[hcsyntax_examples] ?- test_goal 3.

yes

[hcsyntax_examples] ?- test_goal 4.

no (more) solutions

[hcsyntax_examples] ?- test_defcl 4.

yes

[hcsyntax_examples] ?- test_defcl 5.

yes

[hcsyntax_examples] ?- test_defcl 6.

yes

[hcsyntax_examples] ?- test_defcl 7.

no (more) solutions

[hcsyntax_examples] ?- stop.
Teyjus>