/**************************************************************************
*
*     GENERAL LIBRARY FOR THE SCAN - CORRESPONDENCE THEORY PROGRAM 
*
*                         Hans Juergen Ohlbach
*
* This file contains a collection of predefined operators and various 
* other necessary definitions for the translation interface to SCAN. 
*
**************************************************************************/


:-dynamic(define/3).
:-dynamic(define/4).
:-dynamic(define/5).

/**************************************************************************
*
*                           TRUTH CONDITIONS
*
* The truth conditions specify when a formula is to be considered a tautology.
* They are instantiated with the truth_condition predicate. 
*
**************************************************************************/

define(truth_condition,    
	all,                /* Truth in all possible worlds */
	'all world (world |= Phi)').

define(truth_condition,
	initial(0),	    /* Truth in a particular possible world */
	'0 |= Phi').


/* Possible instantiations:
*
*       truth_condition(all).
*       truth_condition(initial(a)).
*/

/**************************************************************************
*
*                            OPERATOR DEFINITIONS
*
* This part contains a rich collection of predefined classical and 
* nonclassical logical connectives. 
*
***************************************************************************/



:-op(780,xfy,connective). /* Dummy connective */


/**************************************************************************
*                               CLASSICAL LOGIC
**************************************************************************/
  

define(operator,unary(operator,unary),             
	'(w |= operator Phi) <-> unary(w |= Phi)',
	op(500,fx,operator)).

/* Prototypic negation sign. 
*  Instantiated with
*
*          operator(unary(-,-)).
*/


define(operator,binary(operator,connective),
	'w |= (Phi operator Psi) <-> (w |= Phi connective w |= Psi)',
	op(800,xfy,operator)).

/* Prototypic classical binary connective.
*  Instantiated with
*
*          operator(binary(&,&),780).          (conjunction)
*          operator(binary('|','|'),790).      (disjunction)
*          operator(binary(->,->),800).        (implication)
*          operator(binary(<->,<->),850).      (equivalence)
*
*/


define(operator,rewrite(change,connective),
	'(P change Q) -> (Q connective P)',
	op(800,yfx,change)).

/* This is an example for a defined connective. 
*  Instantiated with
*
*           operator(rewrite(<=,->)).
*
*  your get a backwards implication. 
*/


define(operator,xor(xor),
	'(P xor Q) -> ((P | Q) & -(P & Q))',
	op(790,yfx,xor)).

/* This is another example for a defined connective
*  which yields the classical exclusive or connective.
* 
*  Instantiated with 
*   
*           operator(xor(xor)).
*/


/**************************************************************************
*                               QUANTIFIERS
**************************************************************************/


define(operator,quantifier(l_quantifier,fol_quantifier),
	'w |= l_quantifier(X,Phi) <-> fol_quantifier(X,w |= Phi)',_).

/* Domain quantifiers with constant domain assumption
*  Instantiated with
*
*            operator(quantifier(all,all)).       (universal quantification)
*            operator(quantifier(exists,exists)). (existential quantification)
*  
*  you get the usual quantifiers as in predicate logic. 
*  The implicit assumption is constant domain, i.e. all worlds have the same domain. 
*/



define(operator,quantifier(l_quantifier,fol_quantifier,ex,connective),
	'w |= l_quantifier(X,Phi) <-> fol_quantifier(X,ex(w,X) connective w |= Phi)',_).

/* Domain quantifiers without the constant domain assumption
*  Instantiated with
*
*            operator(quantifier(all,all,ex,->)).        (universal quantification)
*            operator(quantifier(exists,exists,ex,&)). (existential quantification)
*  
*  you get the quantifiers as in predicate logic, but without the constant domain
*  assumption. Therefore the 'ex' predicate is used as an explicit declaration for 
*  the membership of an object in the domain of a world. 
*  As an example, the formula 'all x p(x)' is translated (in world w) into
*                             'all x ex(w,x) -> p(w,x)'
*  where the now classical quantifier all quantifies over all domain elements of 
*  all worlds and the condition 'ex(w,x)' selects those objects which are in w's domain.
*/


/**************************************************************************
*                               MODAL LOGIC
**************************************************************************/


define(operator,box(b,r),
	'w |= b Phi <-> (all v (r(w,v) -> v |= Phi))',
	op(500,fy,b)).

define(operator,diamond(d,r),
	'w |= d Phi <-> (exists v (r(w,v) & v |= Phi))',
	op(500,fy,d)).

/* These two are the modal operators for normal modal systems with standard 
*  Kripke semantics. 
*  Instantiated for example with:
*
*            operator(box(bx,'R')).
*            operator(diamond(dia,'R')).
*/
define(operator,weydert(i,r,s),
	'w |= (Phi i Psi) <-> (exists v ((r(w,v) & (v |= Phi)) -> (exists w1 ((r(w,w1) -> ((w1 |= Phi) & (all z (r(w,z) -> (((z |= Phi) & s(z,w1)) -> (z |= Psi))))))))))',
        op(800,xfy,i)).



define(operator,box(b,p,r),
	'w |= b(p,Phi) <-> (all v (r(p,w,v) -> v |= Phi))',
	_).

define(operator,diamond(d,p,r),
	'w |= d(p,Phi) <-> (exists v (r(p,w,v) & v |= Phi))',
	_).

/* Here we have the two parameterized modal operators for normal modal systems with standard 
*  Kripke semantics. 
*  Instantiated for example with:
*
*            operator(box(bx,'John','R')).
*            operator(diamond(dia,'John','R')).
*
*  you get versions you may use as belief or knowledge operators. 
*  Alternatively 
*
*            operator(box(bx,belief(X),'R')).
*            operator(diamond(dia,belief(X),'R')).
*
*  give you operators with a term as parameter. 
*  The term contains a variable which may be bound to arbitrary other terms. 
*/


define(operator,boxf(b,apply),
	'w |= b Phi <-> (all gamma (apply(gamma,w) |= Phi))',
	op(500,fy,b)).

define(operator,diamondf(d,apply),
	'w |= d Phi <-> (exists gamma (apply(gamma,w) |= Phi))',
	op(500,fy,d)).


/* These are the two modal operators in the functional language.
*  SERIALITY of the accessibility relation is assumed. 
*  Instantiation:
*
*             operator(boxf(bx,app)).
*             operator(diamondf(dia,app)).
*  
*  Mixing relational box with functional diamond and activating negation normal forming 
*  before translation yields the semi functional translation. 
*/



define(operator,boxf(b,apply,dead_end),
	'w |= b Phi <-> dead_end(w) | (all gamma (apply(gamma,w) |= Phi))',
	op(500,fy,b)).

define(operator,diamondf(d,apply,dead_end),
	'w |= d Phi <-> -dead_end(w) & (exists gamma (apply(gamma,w) |= Phi))',
	op(500,fy,d)).

/* These are the two modal operators in the functional language
*  without the seriality assumption. The dead_end predicate takes care of the
*  non-serial parts of the accessibility relation. 
*  Instantiation:
*
*             operator(boxf(bx,app,de)).
*             operator(diamondf(dia,app,de)).
*/


define(operator,boxfp(b,p,apply),
	'w |= b(p,Phi) <-> (all gamma (apply(p,gamma,w) |= Phi))',
	op(500,fy,b)).

define(operator,diamondfp(d,p,apply),
	'w |= d(p,Phi) <-> (exists gamma (apply(p,gamma,w) |= Phi))',
	op(500,fy,d)).


define(operator,boxfp(b,p,apply,d),
	'w |= b(p,Phi) <-> (d(w,p) -> (all gamma (apply(p,gamma,w) |= Phi)))',
	op(500,fy,b)).

define(operator,diamondfp(d,p,apply,dead_end),
	'w |= d(p,Phi) <-> -dead_end(w,p) & (exists gamma (apply(p,gamma,w) |= Phi))',
	op(500,fy,d)).

/* These are the corresponding extensions of the functional interpretation of the 
*  modal operators to parameterized modal operators. 
*  Instantiation:
*
*             operator(boxfp(bx,'John',app)).
*             operator(diamondfp(dia,'John',app)).
*  
*             operator(boxfp(bx,'John',app,de)).
*             operator(diamondfp(dia,'John',app,de)).
*/





/**************************************************************************
*                               IMPLICATIONS
**************************************************************************/



define(operator,intuitionistic_implication(imp,r),
	'w |= (Phi imp Psi) <-> (all v (r(w,v) -> ((v |= Phi) -> (v |= Psi))))',
	op(800,xfy,imp)).

define(operator,intuitionistic_negation(neg,r),
	'w |= (neg Phi) <-> (all v (r(w,v) -> (-(v |= Phi))))',
	op(500,fx,neg)).




define(operator,relevant_implication(imp,r),
	'w |= (Phi imp Psi) <-> (all u v (r(w,u,v) -> ((u |= Phi) -> (v |= Psi))))',
	op(800,xfy,imp)).

/* These are the most prominent nonclassical implications, intuitionistic and 
*  relevant implications. If you use them, be aware of the other constraints on the 
*  semantics, namely the restrictions on the assignment and the truth condition in 
*  the relevant logic case. 
*  Instantiation
*  
*              operator(intuitionistic_implication(=>,r)).
*              operator(relevant_implication(=>,r)).
*/

define(operator,basic_implication(imp,r),
	'w |= (Phi imp Psi) <-> (all u ((u |= Phi) -> (exists v ((v |= Psi) & r(w,u,v)))))',
	op(800,xfy,imp)). 



/* The following is the truth condition for the conditional operator ``i''
*  in Chellas's basic system CK in terms of selection functions. 
*  There are no conditions on r.
*/

define(operator,chellas(i,r),
        'w |= (A i C) <->  (exists U ((all v (in(v,U) <-> v |= A) & (all u (r(U,w,u) -> u |= C) ))))',
         op(800,xfy,i)).

define(operator,chellas1(i,r),
        'w |= (A i C) <->  (all U ((all v (in(v,U) <-> v |= A)) -> (all u (r(U,w,u) -> u |= C) )))',
         op(800,xfy,i)).



define(operator,chellas0(i,r),
        'w |= (A i C) <->  (all u exists U (all v (in(v,U) <-> v |= A) & (r(U,w,u) -> u |= C) ))',
         op(800,xfy,i)).


/* The following is the truth condition for the conditional operator ``i''
*  in Burgess's basic system CP in terms of partial preorders (without the
*  Limit Assummption). 
*  r must satisfy weak reflexivity wrefl3: 
*	 all w,u ( ( exists v r(w,u,v) ) -> r(w,u,u) ) 
*  and transitivity trans3:
*	 all w,u,v,t ( (r(w,u,v) & r(w,v,t) ) -> r(w,u,t) )  
*/

define(operator,burgess(i,r),
        'w |= (A i C) <-> (all u ( ((exists v r(w,u,v)) & (u |= A)) -> exists v ( (v |= A) & r(w,v,u) & all vs ( ((vs |= A) & r(w,vs,v)) -> (vs |= C) ))))',
         op(800,xfy,i)).



/* The following is the truth condition for the conditional operator ``i''
*  in Burgess's semantics in terms of partial preorders without the
*  Limit Assummption and for the FLAT LANGUAGE. 
*  r must satisfy reflexivity reflexivity(r): 
*	 all u  r(u,u) 
*  and transitivity transitivity(r):
*	 all u,v,t ( (r(u,v) & r(v,t) ) -> r(u,t) )  
*/

define(operator,burgessF(i,r),
        'w |= (A i C) <-> (all u ( (u |= A) -> exists v ( (v |= A) & r(v,u) & all vs ( ((vs |= A) & r(vs,v)) -> (vs |= C) )) ) )',
         op(800,xfy,i)).



/* The following is the truth condition for the conditional operator ``i''
*  in Burgess's semantics in terms of partial preorders with the
*  LIMIT ASSUMPTION: 
*  For every formula  A , 
*     all w,u ( (u |= A & exists v r(w,u,v)) -> 
*      (exists us (r(w,us,u) & us |= A & all uss(uss |= A -> -r(w,uss,u)))))   
*  
*  (In other words,  u  is minimal in  [A]  w.r.t.  r_w.)
*  This condition is not first-order and cannot be expressed here. 
*  
*  r must satisfy weak reflexivity wrefl3(r): 
*	 all w,u ( ( exists v r(w,u,v) ) -> r(w,u,u) ) 
*  and transitivity trans3(r):
*	 all w,u,v,t ( (r(w,u,v) & r(w,v,t) ) -> r(w,u,t) )  
*/

define(operator,burgessL(i,r),
        'w |= (A i C) <-> ( all u ((u |= A) -> ( (exists v r(w,u,v)) & all us((us |= A) -> -r(w,us,u)) ) -> (u |= C) ) )',
         op(800,xfy,i)).

 

/* The following is the truth condition for the conditional operator ``i''
*  in Burgess's semantics in terms of a single partial preorder for the 
*  FLAT LANGUAGE and with the LIMIT ASSUMPTION: 
*  r is a binary relation, and for every formula  A , 
*     all w,u ( (u |= A & exists v r(u,v)) -> 
*      (exists us (r(us,u) & us |= A & all uss(uss |= A -> -r(uss,u)))))   
*  
*  r must satisfy weak reflexivity wrefl(r): 
*	 (all u,v -r(u,v)) | (all u  r(u,u)) 
*  transitivity transitivity(r):
*	 all u,v,t ( (r(u,v) & r(v,t) ) -> r(u,t) )  
*/

define(operator,burgessLF(i,r),
        'w |= (A i C) <-> ( all u ( ((u |= A) & all us((us |= A) -> -r(us,u)) ) -> (u |= C)))',
         op(800,xfy,i)).



/* The following is the truth condition for the conditional operator ``i''
*  in Burgess's basic system CP+(CMP) in terms of partial preorders
*  (without the Limit Assummption) and with WEAK CENTErING. 
*  r must satisfy weak reflexivity wrefl3(r): 
*	 all w,u ( ( exists v r(w,u,v) ) -> r(w,u,u) ) 
*  transitivity trans3(r):
*	 all w,u,v,t ( (r(w,u,v) & r(w,v,t) ) -> r(w,u,t) )  
*  and weak centering wcent3(r):
*	 all w ( r(w,w,w) & all u ( (exists v r(w,u,v)) -> r(w,w,u)) )
*/

define(operator,burgessW(i,r),
        'w |= (A i C) <-> (all v ( ( (r(w,w,v) & v |= A) -> exists u ((u |= A) & r(w,u,v) & all us ( ((us |= A) & r(w,us,u) ) -> (us |= C) )))) )',
         op(800,xfy,i)).




/* The following is the truth condition for the conditional operator ``i''
*  in Lewis's basic system V in terms of total preorders (without the
*  Limit Assummption). 
*  r must satisfy weak reflexivity wrefl3(r): 
*	 all w,u ( ( exists v r(w,u,v) ) -> r(w,u,u) ) 
*  transitivity trans3(r):
*	 all w,u,v,t ( (r(w,u,v) & r(w,v,t) ) -> r(w,u,t) )  
*  and totality total3(r):
*	 all w,u,v ( (r(w,u,v) | r(w,v,u) )  
*/

define(operator,lewis(i,r),
        'w |= (A i C) <-> (all u ( ((exists v r(w,u,v)) & (u |= A)) -> exists v ( (v |= A) & r(w,v,u) & all vs ( ((vs |= A) & r(w,vs,v)) -> (vs |= C) )) ) )',
         op(800,xfy,i)).



/* The following is the truth condition for the conditional operator ``i''
*  in Lewis's basic system V in terms of total preorders for the 
*  FLAT LANGUAGE and with the LIMIT ASSUMPTION.
*  r must satisfy weak reflexivity wrefl(r): 
*	 (all u,v -r(u,v)) | (all u  r(u,u)) 
*  transitivity transitivity(r):
*	 all u,v,t ( (r(u,v) & r(v,t) ) -> r(u,t) )  
*  and totality total(r):
*	 all u,v ( (r(u,v) | r(v,u) )  
*/

define(operator,lewisLF(i,r),
        'w |= (A i C) <-> (all u ( (u |= A) -> exists v ( (v |= A) & r(v,u) & all vs ( (vs |= A) -> -r(vs,v) )) ) )',
         op(800,xfy,i)).


define(operator,lewisL(i,r),
	'w |= (Phi i Psi) <-> (all u (((u |= Phi) & (all v ((v |= Phi) -> r(w,u,v)))) -> (u |= Psi)))',
	 op(800,xfy,i)).


define(operator,burgessOld(i,r),
	'w |= (Phi i Psi) <-> (all u (((u |= Phi) & (all v (((v |= Phi) & (r(w,v,u))) -> r(w,u,v)))) -> (u |= Psi)))',
	 op(800,xfy,i)).



define(operator,limit(i,r),
	'w |= (Phi i Psi) <-> (all u ((u |= Phi) -> (exists v ((v |= Phi) & r(w,v,u) & (all vs ((r(w,vs,v) & (vs |= Phi)) -> (vs |= Psi)))))))',
	 op(800,xfy,i)).




define(operator,chellasOld(i,r),
	'w |= (Phi i Psi) <-> (all w1 ((exists x (r(w,w1,x) & (all v (in(v,x) <-> (v |= Phi))))) -> (w1 |= Psi)))',
	 op(800,xfy,i)).


/**************************************************************************
*                          ARROW LOGIC OPERATORS
**************************************************************************/

define(operator,comp(o,r),
	'w |= (Phi o Psi) <-> (exists u v (r(w,u,v) & (u |= Phi) & (v |= Psi)))',
        op(800,xfy,o)).

define(operator,conv(c,r),
	'w |= (Phi c) <-> (exists u (r(w,u) & (u |= Phi)))',
        op(800,xf,c)).

define(assumption,universal(u),
	'all x u(x)').

/* o is composition and c converse.  E.g.
*	
*	((r o s) c) -> ((s c) o (r c))
*	
* Instantiated with
*
*	operator(comp(o,'C')).
*	operator(conv(c,'F')).
*
* The identity (id) need not be defined as an operator.  The correct
* translation is implicit in the translation of any proposition, namely 
*
*	w |= (id) <-> id(w)
*
* The universal relation, u say, is also translated according to this
* scheme.  Use also the assumption
*
*	universal(u).
*/

/**************************************************************************
*                               TEMPORAL LOGIC
**************************************************************************/

define(operator,until(until,r),
	'w |= (Phi until Psi) <-> (exists v (r(w,v) & v |= Psi & (all u (r(w,u) & r(u,v) -> u |= Phi))))',
	op(700,xfy,until)).

define(operator,since(since,r),
	'w |= (Phi since Psi) <-> (exists v (r(v,w) & v |= Psi & (all u (r(v,u) & r(u,w) -> u |= Phi))))',
	op(700,xfy,since)).

/* Here we have the simplest version of the usual UNTIL and SINCE operators of temporal logic.
*  More sophisticated versions would distinguish open and closed intervals. 
*  Instantiation:
*         
*              operator(until('U','F')).
*              operator(since('S','F')).
*/
	


/**************************************************************************
*                               
*                                  REWRITE SYSTEMS
*
**************************************************************************/


define(rr_rule,cancel(-),
	'-(-P) -> P').

/* Cancelling the negation sign. 
*   Typical instantiation:  cancel(-)
*/

define(rr_rule,neg_in(-,&,'|'),
	 '-(P & Q) -> (-P | -Q)').

/* Moving the negation sign in. 
*  Typical instantiations:  neg_in(-,&,'|') and neg_in(-,'|',&)
*/

define(rr_rule,implication(-,->,&,'|'),
	[ '(P -> Q) -> (-P | Q)',
	 '-(P -> Q) -> (P & -Q)']).


define(rr_rule,equivalence(-,<->,&,'|'),
	[ '(P <-> Q) -> ((-P | Q) & (P | -Q))',
	 '-(P <-> Q) -> ((P | Q) & (-P | -Q))']).


define(rr_rule,quantifier(-,q1,q2),
	'-(q1(X,P)) -> q2(X,-P)').

/* Moving the negation sign over quantifiers
*  Typical instantiations: quantifier(-,all,exists) and quantifier(-,exists,all)
*/

define(rr_rule,ml_in1(-,b,d),
	'-b(Phi) -> d(-Phi)').

define(rr_rule,ml_in2(-,b,d),
	'-b(P,Phi) -> d(P,-Phi)').


/* Moving the negation sign over modal operators
*  Typical instantiations:  ml_in1(-,box,dia)  and ml_in1(-,dia,box)
*                            ml_in2(-,box,dia)  and ml_in2(-,dia,box)
*/


define(rr_system,pl0_nnf(-,&,'|',->,<->),   
	[cancel(-),
	 neg_in(-,&,'|'),neg_in(-,'|',&),
	 implication(-,->,&,'|'),
	 equivalence(-,<->,&,'|')]).

/* Negation normal form for propositional logic */


define(rr_system,pl1_nnf(-,&,'|',->,<->,all,exists), 
	[pl0_nnf(-,&,'|',->,<->),
	 quantifier(-,all,exists),
	 quantifier(-,exists,all)]).

/* Negation normal form for predicate logic */


define(rr_system,ml0_nnf(-,&,'|',->,<->,b,d),
	[pl0_nnf(-,&,'|',->,<->),ml_in1(-,b,d),ml_in1(-,d,b)]).

/* Negation normal form for propositional modal logic */


define(rr_system,ml1_nnf(-,&,'|',->,<->,b,d,all,exists),
	[ml0_nnf(-,&,'|',->,<->,b,d),
	quantifier(-,all,exists),quantifier(-,exists,all)]).

/* Negation normal form for quantified modal logic */





/**************************************************************************
*  
*                    ASSUMPTIONS
*
**************************************************************************/

define(assumption,reflexivity(r),
	'all x r(x,x)').


define(assumption,symmetry(r),
	'all x y (r(x,y) -> r(y,x))').


define(assumption,transitivity(r),
	'all x y z(r(x,y) & r(y,z) -> r(x,z))').

define(assumption,total(r),
		'all u v ( (r(u,v) | r(v,u))').

/*binary weak reflexivity : */
define(assumption,wrefl(r),
		'(all u v (-r(u,v)) | (all u  r(u,u))').


/*ternary weak reflexivity : */
define(assumption,wrefl3(r),
                'all w u ( ( exists v r(w,u,v) ) -> r(w,u,u) )').


/*ternary transitivity :*/
define(assumption,trans3(r),
                'all w u v t ( (r(w,u,v) & r(w,v,t) ) -> r(w,u,t) )').


/*weak centering :*/
define(assumption,wcent3(r),
		'all w ( r(w,w,w) & all u ( (exists v r(w,u,v)) -> r(w,w,u)) )').
/*ternary totality :*/
define(assumption,total3(r),
		'all w u v ( (r(w,u,v) | r(w,v,u) )').

define(assumption,irrefl3(r),'all w -r(w,w,w)').




/**************************************************************************
*  
*                    QUALIFICATIONS
*
**************************************************************************/


define(qualification,assignment_restriction(p,r),
	'all w (p(w) -> (all v (r(w,v) -> p(v))))').

define(qualification,assignment_restriction(p,r,0),
	'all u v (r(0,u,v) & p(u) -> p(v))').


/* Assignment restrictions, typical for intuitionistic logic and relevance logic */


define(qualification,locality(p,ex),
	'all w x (p(w,x) -> ex(w,x))').

/* In quantified modal logic:
*   Declares that predicate p is true at most in the domain of the current world */


define(qualification,generated(p,less),
	'exists t (all x (p(x) <-> less(t,x)))').


/**************************************************************************
*                           DEFAULTS
**************************************************************************/


:- truth_condition(all).