%==============================================================================
% Project:    SLP - An Interpreter for Super Logic Programs / Static Semantics
% Module:     test1.txt
% Purpose:    This is a test for the syntax analysis and clause conversion
% Last Change:12.10.2001
% Language:   SLP
% Author:     Stefan Brass
% Email:      Stefan.Brass@informatik.uni-giessen.de, sbrass@sis.pitt.edu
% Address:    Universitaet Giessen, Arndtstr. 2, 35392 Giessen, Germany
% Copyright:  (c) 2001 by Stefan Brass
% Licence:    Distributed under the conditions of the GNU Public Licence.
%==============================================================================

% All these formulas are syntactically legal an should be accepted:

p_qrst12(a,-234).
p(a,2,X) :- r(X,_,  _X  ,'quoted atom#@!&|~'), ((not s)).
p & q & r.
(p & q) & r.
p & (q & r).
p & q | r.
p | q & r.
p <-> q.
~p(_) <- q(_) & r(_).
p -> s | t.
~~~p.
not p -> s.
not(p & q | r) -> s.
p <- q(X) & not(r(X)).

p <- % Formula is distributed over two lines
	q.

% In this test, it is important to look at the input formulas
% before the conversion into clauses. They should be shown as follows:
%	p_qrst12(a, -234).
%	p(a, 2, X) :- r(X, _, _X, 'quoted atom#@!&|~') & not s.
%	p & q & r.
%	(p & q) & r.
%	p & q & r.
%	p & q | r.
%	p | q & r.
%	p <-> q.
%	~p(_) <- q(_) & r(_).
%	p -> s | t.
%	~~~p.
%	not p -> s.
%	not(p & q | r) -> s.
%	p <- q(X) & not r(X).
%	p <- q.

% The resulting facts should be (note that nonminimal facts are deleted):
%	p_qrst12(a, -234).
%	p.
%	q.
%	r.
%	s <- not p.
%	s <- not(p & q), not r.

% The resulting rules should be
%	p(a, 2, X) :- r(X, _, _X, 'quoted atom#@!&|~'), not s.
%	p <- q.
%	q <- p.
%	FALSE <- p(_) & q(_) & r(_).
%	s | t <- p.
%	FALSE <- p.
%	p <- q(X) & not r(X).
%	p <- q.

% The result of hyperresolution is:
%	FALSE.

$v.