/* --- Copyright University of Sussex 1989. All rights reserved. ----------
 > File:            $poplocal/local/plog/lib/checker.pl
 > Purpose:         Interactive proof checker for first-order logic.
 > Author:          Harry Barrow, Jan 31 1989 (see revisions)
 > Documentation:   TEACH * CHECKER
 > Related Files:
 */


/* Representation:

    Clauses are represented internally as lists of literals.
    Negated literals are indicated by the prefix -
    Clauses are stored under a name.
    The source of a clause is also recorded.

        a_clause(Name,TheClause).
        clause_source(Name,Source).

*/



/* Erase the database and initialise the proof checker.
*/
initialise_prover :-
    retractall(a_clause(_,_)),
    retractall(clause_source(_,_)),
    retractall(number_of_clauses(_)),
    assert(number_of_clauses(0)).



/* Add a new clause to the database
*/
add_clause(Name,Clause,Source) :-
    number_new_clause(N),
    name_clause(N,Name),
    assertz(a_clause(Name,Clause)),
    assertz(clause_source(Name,Source)).


/* Add a list of clauses to the database
*/
add_clauses([],Source).
add_clauses([Clause|Clauses],Source) :-
    add_clause(Name,Clause,Source),
    add_clauses(Clauses,Source).


/* Delete a clause from the database
*/
delete_clause(Name) :-
    retract(a_clause(Name,_)),
    retract(clause_source(Name,_)),
    !.


/* Generate a number for a new clause
*/
number_new_clause(N1) :-
    retract(number_of_clauses(N)),
    N1 is N + 1,
    assert(number_of_clauses(N1)),
    !.


/* Generate a clause name if needed
*/
name_clause(N,Name) :- nonvar(Name), !.         % It has a name
name_clause(N,clause(N)).                       % call it clause(N)



/* Check to see if a clause is null, and say so if it is
*/
check_answer(Name) :-
    a_clause(Name,[]),
    nl(1),write('The null clause -- proof complete'),nl(1).
check_answer(Name) :-
    a_clause(Name,[answer(X)]),
    nl(1),write('The answer is:'),nl(1),
    write(X),nl(1),write('-- proof complete'),nl(1).
check_answer(Name).



/* Print a clause.
*/
print_clause(Name) :-
    a_clause(Name,Clause),
    write(Name),write(': '),write(Clause),
    clause_source(Name,Source),
    write(' -- '), write(Source),nl(1).



/* Print all clauses in the database.
*/
print_clauses :-
    nl(1),
    print_clause(Name),
    fail.
print_clauses :-
    nl(1).


/* Unify two literals.
*/
unify_literals(-(L1),L2) :- unify_terms(L1,L2).
unify_literals(L1,-(L2)) :- unify_terms(L1,L2).


/* Unify two terms (no negations involved)
*/
unify_terms(L1,L2) :-
    var(L1), var(L2), !, L1=L2.
unify_terms(L1,L2) :-
    var(L1), !, \+(occurs_in(L1,L2)), L1=L2.
unify_terms(L1,L2) :-
    var(L2), !, \+(occurs_in(L2,L1)), L1=L2.
unify_terms(L1,L2) :-
    functor(L1,Fn,Arity), functor(L2,Fn,Arity), unify_args(Arity,L1,L2).

unify_args(0,L1,L2) :- !.
unify_args(ArgN,L1,L2) :-
    arg(ArgN,L1,Arg1),
    arg(ArgN,L2,Arg2),
    unify_terms(Arg1,Arg2),
    ArgN1 is ArgN - 1,
    unify_args(ArgN1,L1,L2).


/* Check whether a variable occurs in a term
*/
occurs_in(Var,Term) :-
    var(Term), !, Var == Term.
occurs_in(Var,Term) :-
    functor(Term,Fn,Arity),
    occurs_in_arg(Var,Arity,Term).

occurs_in_arg(Var,0,Term) :- !,
    fail.
occurs_in_arg(Var,ArgN,Term) :-
    arg(ArgN,Term,Arg),
    occurs_in(Var,Arg).
occurs_in_arg(Var,ArgN,Term) :-
    ArgN1 is ArgN -1,
    occurs_in_arg(Var,ArgN1,Term).



/* Some utility procedures */


/* Find the nth element of a list.
*/
nth(1,[X|L],X).
nth(N,[X|L],Y) :- N1 is N-1, nth(N1,L,Y).


/* Remove the nth element of a list.
*/
remove_nth(1,[X|L],L).
remove_nth(N,[X|L],[X|L1]) :- N1 is N-1, remove_nth(N1,L,L1).


/* Append two lists
*/
append([],L,L).
append([X|L1],L2,[X|L0]) :- append(L1,L2,L0).


/* Test whether an item already exists in a list -- without unifying
*/
member_eq(X,[Y | List]) :- X == Y, !.
member_eq(X,[Y | List]) :- member_eq(X,List).




/* Test that a Prolog goal is achievable, but backtrack to ensure
    that no variables remain bound.
    E.g.  could(unify_literals(L1,L2)) has the effect of checking
    for unifiability without binding any variables.

    (Warning: any database changes will not be undone, so use wisely!)
*/
could(X) :-  \+( \+(X) ).           % just  not not X



/* The main resolution step.
*/
resolve(NC1,NL1,NC2,NL2,NewName) :-
    a_clause(NC1,C1),
    a_clause(NC2,C2),
    nth(NL1,C1,L1),
    nth(NL2,C2,L2),
    unify_literals(L1,L2),
    remove_nth(NL1,C1,RC1),
    remove_nth(NL2,C2,RC2),
    unite_clauses(RC1,RC2,RC),
    add_clause(NewName,RC,resolve(NC1,NL1,NC2,NL2)).

res(NC1,NL1,NC2,NL2,NewName) :-
    resolve(NC1,NL1,NC2,NL2,NewName),
    print_clause(NewName),
    check_answer(NewName).

res(NC1,NL1,NC2,NL2) :-
    res(NC1,NL1,NC2,NL2,NewName).


/* Factor a clause.  I.e. unify two of its terms
*/
factor(NC1,NL1,NL2,NewName) :-
    a_clause(NC1,C1),
    nth(NL1,C1,L1),
    nth(NL2,C1,L2),
    unify_terms(L1,L2),
    remove_nth(NL1,C1,RC1),
    add_clause(NewName,RC1,factor(NC1,NL1,NL2)).

fac(NC1,NL1,NL2,NewName) :-
    factor(NC1,NL1,NL2,NewName),
    print_clause(NewName),
    check_answer(NewName).

fac(NC1,NL1,NL2) :-
    fac(NC1,NL1,NL2,NewName).



/* Form the union of two clauses (omitting repeated literals)
*/
unite_clauses([],Clause,Clause).
unite_clauses([Literal | Literals],Clause,Union) :-
    member_eq(Literal,Clause), !,
    unite_clauses(Literals,Clause,Union).
unite_clauses([Literal | Literals],Clause,[Literal | Union]) :-
    unite_clauses(Literals,Clause,Union).


/* Simple test examples
    Set up an example by calling    example(1).  etc.
*/

/* Elementary proof in two steps
    Given:  Socrates is human           human(socrates)
            All humans are mortal       human(X) => mortal(X)
    Prove:  Socrates is mortal          mortal(socrates)
*/
example(1) :-
    initialise_prover,
    add_clause(hum_soc, [human(socrates)],axiom),
    add_clause(mortality,[-human(X),mortal(X)],axiom),
    add_clause(mort_soc,[-mortal(socrates)],goal),
    print_clauses.


/*  I have two keys and I know one of them fits a door, but I
    do not know which.  I also know that if I have a key that
    fits the door, then I can open the door.
    Prove that I can indeed open the door.
*/
example(2) :-
    initialise_prover,
    add_clause(have_key1,[have(key1)],axiom),
    add_clause(have_key2,[have(key2)],axiom),
    add_clause(can_open, [-have(Key),-fits(Key,Door),can_open(Door)],axiom),
    add_clause(one_opens,[fits(key1,door),fits(key2,door)],axiom),
    add_clause(open_goal,[-can_open(door)],goal),
    print_clauses.


/* Description of the prolog procedure append in logic,
    Given:  append([],L,L).
            append([X|L1],L2,[X|L0]) <= append(L1,L2,L0).
            answer(List) <= append([a,b],[c,d],List)
    Derive: answer(List)
    (Beware of infinite chains of inference!)
*/
example(3) :-
    initialise_prover,
    add_clause(app_nil, [append([],L,L)],axiom),
    add_clause(app_list,[append([X|L1],L2,[X|L0]),-append(L1,L2,L0)],axiom),
    add_clause(app_ans,[-append([a,b],[c,d],List),answer(List)],goal),
    print_clauses.



/*  A robot world example.  There are two places, here and there, and a
    robot hand which can perform the operations pickup, letgo, and goto.
    The operations are applied to a state to give a new state.
    E.g.  pickup(state0) is the state resulting from doing pickup in state0.
    There is also a brick for the robot to handle.
*/
example(4) :-
    initialise_prover,
    % operation pickup
    add_clause(pickup_at,
        [-at(Thing,Place,State),at(Thing,Place,pickup(State))],axiom),
    add_clause(pickup_hand,
        [-at_hand(Place,State),at_hand(Place,pickup(State))],axiom),
    add_clause(pickup_held,
        [-at(Thing,Place,State),-at_hand(Place,State),-empty_hand(State),
            holding(Thing,pickup(State))],axiom),
    % operation letgo
    add_clause(letgo_at,
        [-at(Thing,Place,State),at(Thing,Place,letgo(State))],axiom),
    add_clause(letgo_hand,
        [-at_hand(Place,State),at_hand(Place,letgo(State))],axiom),
    add_clause(letgo_held,
        [-holding(Thing,State),empty_hand(letgo(State))],axiom),
    % operation goto
    add_clause(goto_hand,
        [at_hand(Place,goto(Place,State))],axiom),
    add_clause(goto_held,
        [-holding(Thing,State),holding(Thing,goto(Place,State))],axiom),
    add_clause(goto_empty,
        [-empty_hand(State),empty_hand(goto(Place,State))],axiom),
    % holding something
    add_clause(hold_at,
        [-holding(Thing,State),-at_hand(Place,State),at(Thing,Place,State)],axiom),
    % initial state of the world
    add_clause(brick_start,[at(brick,here,start)],axiom),
    add_clause(hand_start,[at_hand(here,start)],axiom),
    add_clause(empty_start,[empty_hand(start)],axiom),
    % goal state
    add_clause(goal,
        [-at(brick,there,State),answer(State)],goal),

    print_clauses.

/* --- Revision History ---------------------------------------------------
--- Harry Barrow, Feb  1 1989
--- Harry Barrow, Jan 31 1989
 */
