:-dynamic initiation/2, termination/2, happens/2, tprop/1, ram/1.

/* 

EXAMPLE 1
---------

E Language formulation:

injectA "initiates" protected "when" type0
injectB "initiates" protected "when" not type0


injectA "happens-at" 2 
injectB "happens-at" 3 


Logic programming-based formulation:

*/

initiation(protected,T) :- happens(injectA,T),holds(type0,T), true.
initiation(protected,T) :- happens(injectB,T),neg(holds(type0,T)), true.

happens(injectA,2).
happens(injectB,3).


%Should be able to infer: credulous([holds(protected,0)]) 
%Should be able to infer: credulous([holds(protected,1)]) 
%Should be able to infer: credulous([holds(protected,2)]) 
%Should be able to infer: credulous([holds(protected,3)]) 
%Should be able to infer: credulous([neg(holds(protected,0))]) 
%Should be able to infer: credulous([neg(holds(protected,1))]) 
%Should be able to infer: credulous([neg(holds(protected,2))]) 
%Should be able to infer: credulous([neg(holds(protected,3))]) 
%Should be able to infer: sceptical([holds(protected,4)]) 
%Should be able to infer: sceptical([holds(protected,5)]) 
%Shouldn't be able to infer: sceptical([neg(holds(protected,4))]) 
%Shouldn't be able to infer: sceptical([neg(holds(protected,5))]) 



/* 
EXAMPLE 2 
---------

E Language formulation:

take "initiates" picture "when" loaded

take "happens-at" 2 

not picture "holds-at" 1
picture "holds-at" 3

Logic programming-based formulation:
*/

initiation(picture,T) :- happens(take,T),holds(loaded,T), true.

happens(take,2).

tprop(neg(holds(picture,1))).
tprop(holds(picture,3)).

%Should be able to infer: sceptical([holds(loaded,2)])
%Should be able to infer: sceptical([holds(loaded,0)])
%Should be able to infer: sceptical([holds(loaded,1)])
%Should be able to infer: sceptical([holds(loaded,3)])
%Should be able to infer: sceptical([holds(loaded,4)])

/*
EXAMPLE 2+
----------

E Language formulation: remove from the above

not picture "holds-at" 1

*/

%Shouldn't be able to infer: sceptical([holds(loaded,0)])
%Shouldn't be able to infer: sceptical([holds(loaded,1)])
%Shouldn't be able to infer: sceptical([holds(loaded,2)])
%Shouldn't be able to infer: sceptical([holds(loaded,3)])
%Shouldn't be able to infer: sceptical([holds(loaded,4)])
%Should be able to infer: credulous([holds(loaded,0)])
%Should be able to infer: credulous([holds(loaded,1)])
%Should be able to infer: credulous([holds(loaded,2)])
%Should be able to infer: credulous([holds(loaded,3)])
%Should be able to infer: credulous([holds(loaded,4)])
%Should be able to infer: credulous([neg(holds(loaded,0))])
%Should be able to infer: credulous([neg(holds(loaded,1))])
%Should be able to infer: credulous([neg(holds(loaded,2))])
%Should be able to infer: credulous([neg(holds(loaded,3))])
%Should be able to infer: credulous([neg(holds(loaded,4))])

/*
EXAMPLE 2++
-----------

E Language formulation: add to the original 

take initiates picture when digital

*/

%Shouldn't be able to infer: sceptical([holds(loaded,0)])
%Shouldn't be able to infer: sceptical([holds(loaded,1)])
%Shouldn't be able to infer: sceptical([holds(loaded,2)])
%Shouldn't be able to infer: sceptical([holds(loaded,3)])
%Shouldn't be able to infer: sceptical([holds(loaded,4)])
%Shouldn't be able to infer: sceptical([holds(digital,0)])
%Shouldn't be able to infer: sceptical([holds(digital,1)])
%Shouldn't be able to infer: sceptical([holds(digital,2)])
%Shouldn't be able to infer: sceptical([holds(digital,3)])
%Shouldn't be able to infer: sceptical([holds(digital,4)])
%Should be able to infer: credulous([holds(loaded,0)])
%Should be able to infer: credulous([holds(loaded,1)])
%Should be able to infer: credulous([holds(loaded,2)])
%Should be able to infer: credulous([holds(loaded,3)])
%Should be able to infer: credulous([holds(loaded,4)])
%Should be able to infer: credulous([holds(digital,0)])
%Should be able to infer: credulous([holds(digital,1)])
%Should be able to infer: credulous([holds(digital,2)])
%Should be able to infer: credulous([holds(digital,3)])
%Should be able to infer: credulous([holds(digital,4)])


/* 
EXAMPLE 3 
---------

E Language formulation:

turnon "initiates" running "when" petrol
turnoff "terminates" running 
empty "terminates" petrol

not running "whenever" not petrol, ok

turnoff "happens-at" 2
turnon "happens-at" 5
empty "happens-at" 8

running "holds-at" 1

Logic programming-based formulation:
*/

initiation(running,T) :- happens(turnon,T),holds(petrol,T), true.
termination(running,T):- happens(turnoff,T), true.
termination(petrol,T):- happens(empty,T), true.

ram(neg(holds(running,T))):-neg(holds(petrol,T)).

happens(turnoff,2).
happens(turnon,5).
happens(empty,8).

tprop(holds(running,1)).

%Should be able to infer: sceptical([holds(running,0)])
%Should be able to infer: sceptical([neg(holds(running,3))])
%Should be able to infer: sceptical([holds(running,6)])
%Should be able to infer: sceptical([neg(holds(running,10))])
%Shouldn't be able to infer: sceptical([neg(holds(running,0))])
%Shouldn't be able to infer: sceptical([holds(running,3)])
%Shouldn't be able to infer: sceptical([neg(holds(running,6))])
%Shouldn't be able to infer: sceptical([holds(running,10)])
%Should be able to infer: sceptical([holds(petrol,0)])
%Should be able to infer: sceptical([holds(petrol,3)])
%Should be able to infer: sceptical([holds(petrol,6)])
%Should be able to infer: sceptical([neg(holds(petrol,10))])
%Shouldn't be able to infer: sceptical([neg(holds(petrol,0))])
%Shouldn't be able to infer: sceptical([neg(holds(petrol,3))])
%Shouldn't be able to infer: sceptical([neg(holds(petrol,6))])
%Shouldn't be able to infer: sceptical([holds(petrol,10)])

/* 
EXAMPLE 4 (WITHOUT T-PROPOSITIONS)
----------------------------------    

E Language formulation:

press "initiates" on 

Logic programming-based formulation:
*/

initiation(on,T) :- happens(press,T), true.

%Shouldn't be able to infer: sceptical([holds(press,7)])
%Should be able to infer: credulous([holds(press,7)])
%Shouldn't be able to infer: sceptical([neg(holds(press,7))])
%Should be able to infer: credulous([neg(holds(press,7))])


/* 
EXAMPLE 5 (WITHOUT T-PROPOSITIONS)
----------------------------------  

E Language formulation:

press "initiates" on  
press "happens-at" 3

Logic programming-based formulation:
*/

initiation(on,T) :- happens(press,T), true.
happens(press,3).

%Should be able to infer: sceptical([holds(on,7)])  
%Should be able to infer: credulous([holds(on,7)]) 
%Shouldn't be able to infer: sceptical([neg(holds(on,7))]) 
%Shouldn't be able to infer: credulous([neg(holds(on,7))]) 


/* 
EXAMPLE 6 (WITHOUT T-PROPOSITIONS)
----------------------------------   

E Language formulation:

press "initiates" on
release "terminates" on
press "happens-at" 3
release "happens-at" 5

Logic programming-based formulation:
*/

initiation(on,T) :- happens(press,T), true.
termination(on,T) :- happens(release,T), true.  
happens(press,3).
happens(release,5).

%Should be able to infer: sceptical([neg(holds(on,7))]) 
%Should be able to infer: credulous([neg(holds(on,7))])
%Shouldn't be able to infer: sceptical([holds(on,7)])
%Shouldn't be able to infer: credulous([holds(on,7)]) 

/* 
EXAMPLE 7 (WITHOUT T-PROPOSITIONS)
----------------------------------  

E Language formulation:

press "initiates" on "when" connected
press "happens-at" 3

Logic programming-based formulation:
*/


initiation(on,T) :- happens(press,T), holds(connected,T), true.
happens(press,3).

%Shouldn't be able to infer: sceptical([neg(holds(on,7))])
%Should be able to infer: credulous([neg(holds(on,7))])
%Shouldn't be able to infer: sceptical([holds(on,7)])
%Should be able to infer: credulous([holds(on,7)])


/* 
EXAMPLE 8 (WITHOUT T-PROPOSITIONS)
---------------------------------- 

E Language formulation:

connect "initiates" connected
press "initiates"  on  "when" connected
connect "happens-at" 2
press "happens-at" 3

Logic programming-based formulation:
*/

initiation(connected,T) :- happens(connect,T), true.
initiation(on,T) :- happens(press,T),holds(connected,T), true.
happens(connect,2).
happens(press,3).

%Should be able to infer: sceptical([holds(on,7)]) 
%Should be able to infer: credulous([holds(on,7)]) 
%Shouldn't be able to infer: sceptical([neg(holds(on,7))])
%Shouldn't be able to infer: credulous([neg(holds(on,7))]) 
%Should be able to infer: sceptical([holds(connected,7)]) 
%Should be able to infer: credulous([holds(connected,7)])
%Shouldn't be able to infer: sceptical([neg(holds(connected,7))])
%Shouldn't be able to infer: credulous([neg(holds(connected,7))])


/* 
EXAMPLE 9 (WITHOUT T-PROPOSITIONS)
----------------------------------   

E Language formulation:

injectA "initiates" protected "when" type0
injectB "initiates"  protected  "when" not type0
injectA "happens-at" 2
injectB "happens-at" 3

Logic programming-based formulation:
*/

initiation(protected,T) :- happens(injectA,T),holds(typeO,T), true.
initiation(protected,T) :- happens(injectB,T),neg(holds(typeO,T)), true.
happens(injectA,2).
happens(injectB,3).

%Should be able to infer: sceptical([holds(protected,7)])
%Should be able to infer: credulous([holds(protected,7)])
%Shouldn't be able to infer: sceptical([neg(holds(protected,7))])
%Shouldn't be able to infer: credulous([neg(holds(protected,7))])


/* 
EXAMPLE 10 (WITH T-PROPOSITIONS)
--------------------------------    

E Language formulation:

press "initiates" on "when" connected
press "happens-at" 3
connected "holds-at" 3

Logic programming-based formulation:

*/

initiation(on,T) :- happens(press,T), holds(connected,T), true.
happens(press,3).
tprop(holds(connected,3)).

%Should be able to infer: sceptical([holds(on,7)])
%Should be able to infer: credulous([holds(on,7)])
%Shouldn't be able to infer: sceptical([neg(holds(on,7))])
%Shouldn't be able to infer: credulous([neg(holds(on,7))])
%Should be able to infer: sceptical([holds(connected,7)])
%Should be able to infer: credulous([holds(connected,7)])
%Shouldn't be able to infer: sceptical([neg(holds(connected,7))])
%Shouldn't be able to infer: credulous([neg(holds(connected,7))])
%Should be able to infer: sceptical([holds(connected,1)]) 
%Should be able to infer: credulous([holds(connected,1)])
%Shouldn't be able to infer: sceptical([neg(holds(connected,1))])
%Shouldn't be able to infer: credulous([neg(holds(connected,1))]) 
%Shouldn't be able to infer: sceptical([holds(on,1)])
%Should be able to infer: credulous([holds(on,1)])
%Shouldn't be able to infer: sceptical([neg(holds(on,1))])
%Should be able to infer: credulous([neg(holds(on,1))])


/* 
EXAMPLE 11 (WITH T-PROPOSITIONS)
--------------------------------    
E Language formulation:

press "initiates" on "when" connected
press "happens-at" 3
connected "holds-at" 2

Logic programming-based formulation:
*/

initiation(on,T) :- happens(press,T),holds(connected,T), true.
happens(press,3).
tprop(holds(connected,2)).


%Should be able to infer: sceptical([holds(on,7)])
%Should be able to infer: credulous([holds(on,7)])
%Shouldn't be able to infer: sceptical([neg(holds(on,7))])
%Shouldn't be able to infer: credulous([neg(holds(on,7))])
%Should be able to infer: sceptical([holds(connected,7)]) 
%Should be able to infer: credulous([holds(connected,7)])
%Shouldn't be able to infer: sceptical([neg(holds(connected,7))])
%Shouldn't be able to infer: credulous([neg(holds(connected,7))])
%Should be able to infer: sceptical([holds(connected,1)])
%Should be able to infer: credulous([holds(connected,1)])
%Shouldn't be able to infer: sceptical([neg(holds(connected,1))])
%Shouldn't be able to infer: credulous([neg(holds(connected,1))])
%Shouldn't be able to infer: sceptical([holds(on,1)])
%Should be able to infer: credulous([holds(on,1)])
%Shouldn't be able to infer: sceptical([neg(holds(on,1))])
%Should be able to infer: credulous([neg(holds(on,1))])

/* 
EXAMPLE 12 (WITH T-PROPOSITIONS)
--------------------------------     
E Language formulation:

take "initiates" picture "when" loaded
take "happens-at" 3
not picture "holds-at" 1
picture "holds-at" 5

Logic programming-based formulation:
*/

initiation(picture,T) :- happens(take,T),holds(loaded,T), true.
happens(take,3).
tprop(neg(holds(picture,1))).
tprop(holds(picture,5)).

%Should be able to infer: sceptical([holds(loaded,1)])
%Should be able to infer: credulous([holds(loaded,1)])
%Shouldn't be able to infer: sceptical([neg(holds(loaded,1))])
%Shouldn't be able to infer: credulous([neg(holds(loaded,1))])
%Should be able to infer: sceptical([holds(loaded,3)])
%Should be able to infer: credulous([holds(loaded,3)])
%Shouldn't be able to infer: sceptical([neg(holds(loaded,3))])
%Shouldn't be able to infer: credulous([neg(holds(loaded,3))])
%Should be able to infer: sceptical([holds(loaded,5)])
%Should be able to infer: credulous([holds(loaded,5)])
%Shouldn't be able to infer: sceptical([neg(holds(loaded,5))])
%Shouldn't be able to infer: credulous([neg(holds(loaded,5))])

/* 
EXAMPLE 13 (WITH T-PROPOSITIONS)
--------------------------------     

take1 "initiates" picture "when" loaded1
take2 "initiates" picture "when" loaded2

take1 "happens-at" 3
take2 "happens-at" 4

not  picture "holds-at" 1
picture "holds-at" 5

Logic-programming-based translation:
*/


initiation(picture,T) :- happens(take1,T),holds(loaded1,T), true.
initiation(picture,T) :- happens(take2,T),holds(loaded2,T), true.
happens(take1,3).
happens(take2,4).
tprop(neg(holds(picture,1))).
tprop(holds(picture,5)).


%Shouldn't be able to infer: sceptical([holds(loaded1,6)])
%Should be able to infer: credulous([holds(loaded1,6)])
%Shouldn't be able to infer: sceptical([holds(loaded2,6)])
%Should be able to infer: credulous([holds(loaded2,6)])
%Shouldn't be able to infer: sceptical([holds(loaded1,1)])
%Should be able to infer: credulous([holds(loaded1,1)])
%Shouldn't be able to infer: sceptical([holds(loaded2,1)])
%Should be able to infer: credulous([holds(loaded2,1)])

/*
EXAMPLE 14 (WITH T-PROPOSITIONS)
--------------------------------

expose "initiates" infected "when" typeA

expose "happens-at" 3

not  infected "holds-at" 1
infected "holds-at" 6

Logic-programming-based translation:
*/


initiation(infected,T) :- happens(expose,T),holds(typeA,T), true.

happens(expose,3).

tprop(neg(holds(infected,1))).
tprop(holds(infected,6)).


%Should be able to infer: sceptical([holds(typeA,3)])
%Should be able to infer:  sceptical([holds(typeA,1)])
%Should be able to infer:  sceptical([holds(typeA,7)])

/*
EXAMPLE 15 (WITH T-PROPOSITIONS)
--------------------------------

expose "initiates" infected "when" typeA

expose "happens-at" 3

infected "holds-at" 6

Logic-programming-based translation:
*/


initiation(infected,T) :- happens(expose,T),holds(typeA,T), true.

happens(expose,3).

tprop(holds(infected,6)).


%Shouldn't be able to infer: sceptical([holds(typeA,3)])
%Should be able to infer: credulous([holds(typeA,3)])
%Shouldn't be able to infer: sceptical([holds(typeA,7)])
%Should be able to infer: credulous([holds(typeA,7)])

/*
EXAMPLE 16 (WITH T-PROPOSITIONS)
--------------------------------

expose "initiates" infected "when" typeA
expose "initiates" infected "when" typeB
injectA "initiates" danger "when" typeA
injectA "initiates" danger "when" typeB

expose "happens-at" 3
injectA "happens-at" 3

not infected "holds-at" 1
infected "holds-at" 6

Logic-programming-based translation:
*/

initiation(infected,T) :- happens(expose,T),holds(typeA,T), true.
initiation(infected,T) :- happens(expose,T),holds(typeB,T), true.
initiation(danger,T) :- happens(injectA,T),holds(typeA,T), true.
initiation(danger,T) :- happens(injectA,T),holds(typeB,T), true.

happens(expose,3).
happens(injectA,4).

tprop(neg(holds(infected,1))).
tprop(holds(infected,6)).

%Should be able to infer: sceptical([holds(danger,5)])
%Shouldn't be able to infer: sceptical([holds(danger,4)])



/* 
EXAMPLE 17 (WITH RAMIFICATIONS)
-------------------------------

E Language formulation:

turnon "initiates" running "when" petrol
empty "terminates" petrol

fumes "whenever" running 

turnon "happens-at" 3 

not fumes "holds-at" 1

Logic programming-based formulation:

*/

initiation(running,T) :- happens(turnon,T),holds(petrol,T), true.
termination(petrol,T):- happens(empty,T), true.

ram(holds(fumes,T)):-holds(running,T).

happens(turnon,3).

tprop(neg(holds(fumes,1))). 

%Shouldn't be able to infer: sceptical([holds(petrol,3)])
%Shouldn't be able to infer: sceptical([neg(holds(petrol,3))])
%Should be able to infer: credulous([holds(petrol,3)])
%Should be able to infer: credulous([neg(holds(petrol,3))])
%Shouldn't be able to infer: sceptical([holds(petrol,5)])
%Shouldn't be able to infer: sceptical([neg(holds(petrol,5))])
%Should be able to infer: credulous([holds(petrol,5)])
%Should be able to infer: credulous([neg(holds(petrol,5))])
%Shouldn't be able to infer: sceptical([holds(running,1)])
%Should be able to infer: sceptical([neg(holds(running,1))]) 
%Shouldn't be able to infer: credulous([holds(running,1)]) 
%Should be able to infer: credulous([neg(holds(running,1))]) 



/* 
EXAMPLE 18 (WITH RAMIFICATIONS)
-------------------------------  

E Language formulation:

turnon "initiates" running "when" petrol
empty "terminates" petrol

petrol "whenever" running 
not running "whenever" not petrol 

turnon "happens-at" 3 
empty "happens-at" 6 

petrol "holds-at" 1

Logic programming-based formulation:
*/

initiation(running,T) :- happens(turnon,T),holds(petrol,T), true.
termination(petrol,T):- happens(empty,T), true.

ram(holds(petrol,T)):-holds(running,T).
ram(neg(holds(running,T))):-neg(holds(petrol,T)).

happens(turnon,3).
happens(empty,6).

tprop(holds(petrol,1)).

%Shouldn't be able to infer: sceptical([holds(running,8)])
%Shouldn't be able to infer: credulous([holds(running,8)])
%Should be able to infer: sceptical([neg(holds(running,8))])
%Should be able to infer: credulous([neg(holds(running,8))])
%Should be able to infer: sceptical([holds(running,5)])
%Should be able to infer:  credulous([holds(running,5)])
%Shouldn't be able to infer: sceptical([holds(running,2)])
%Should be able to infer:  credulous([holds(running,2)])
%Should be able to infer: sceptical([holds(petrol,5)])
%Should be able to infer: credulous([holds(petrol,5)])

/* 
EXAMPLE 19 (WITH RAMIFICATIONS)
-------------------------------     

E Language formulation:

turnon "initiates" running "when" petrol
empty "terminates" petrol
okon "initiates" ok "when" fine

petrol "whenever" running
fumes "whenever" running
not indicator "whenever" petrol, ok

okon "happens-at" 2
turnon "happens-at" 3
empty "happens-at" 6

not fumes "holds-at" 1

Logic programming-based formulation:
*/

initiation(running,T) :- happens(turnon,T),holds(petrol,T), true.
termination(petrol,T):- happens(empty,T), true.
initiation(ok,T):- happens(okon,T), holds(fine,T),true.

ram(holds(petrol,T)):-holds(running,T).
ram(holds(fumes,T)):-holds(running,T).
ram(neg(holds(indicator,T))):-holds(petrol,T),holds(ok,T).

happens(okon,2).
happens(turnon,3).
happens(empty,6).

tprop(neg(holds(fumes,1))).

%Shouldn't be able to infer: credulous([holds(petrol,0)])
%Shouldn't be able to infer: credulous([holds(petrol,1)])
%Shouldn't be able to infer: credulous([holds(petrol,2)])
%Shouldn't be able to infer: credulous([holds(petrol,3)])
%Shouldn't be able to infer: credulous([holds(petrol,4)])
%Shouldn't be able to infer: credulous([holds(petrol,5)])
%Shouldn't be able to infer: credulous([holds(petrol,6)])
%Shouldn't be able to infer: credulous([holds(petrol,7)])
%Shouldn't be able to infer: sceptical([holds(petrol,7)])
%Should be able to infer: credulous([neg(holds(petrol,7))])
%Shouldn't be able to infer: credulous([holds(running,7)])
%Shouldn't be able to infer: credulous([holds(running,2)])
%Shouldn't be able to infer: credulous([holds(running,4)])
%Shouldn't be able to infer: credulous([holds(running,1)])
%Should be able to infer: credulous([holds(fine,1)])
%Should be able to infer: credulous([holds(fine,7)])
%Should be able to infer: credulous([neg(holds(fine,1))])
%Should be able to infer: credulous([neg(holds(fine,7))])
%Shouldn't be able to infer: sceptical([holds(fine,1)])
%Shouldn't be able to infer: sceptical([holds(fine,7)])



/*
EXAMPLE 20 (WITH RAMIFICATIONS)
------------------------------

E Language formulation:

expose "initiates" infected "when" typeA
expose "initiates" infected "when" typeB
injectA "initiates" danger "when" typeA
injectA "initiates" danger "when" typeB

allergic "whenever" typeA,infected
allergic "whenever" typeB

expose "happens-at" 3
inject "happens-at" 4

not infected "holds-at" 1
infected "holds-at" 6

Logic programming-based formulation:
*/

initiation(infected,T) :- happens(expose,T),holds(typeA,T), true.
initiation(infected,T) :- happens(expose,T),holds(typeB,T), true.
initiation(danger,T) :- happens(injectA,T),holds(typeA,T), true.
initiation(danger,T) :- happens(injectA,T),holds(typeB,T), true.

happens(expose,3).
happens(injectA,4).

tprop(neg(holds(infected,1))).
tprop(holds(infected,6)).

ram(holds(allergic,T)):-holds(typeA,T),holds(infected,T).
ram(holds(allergic,T)):-holds(typeB,T).


%Shouldn't be able to infer: sceptical([holds(allergic,3)])
%Should be able to infer: sceptical([holds(allergic,4)])
%Should be able to infer: sceptical([holds(allergic,5)])
%Should be able to infer: sceptical([holds(allergic,6)])



/*
EXAMPLE 21 (WITH RAMIFICATIONS AND POTENTIAL LOOPING PROBLEMS)
------------------------------

E Language formulation:

     correct happens-at 3
     correct initiates ok
     fine whenever {good}
     good whenever {ok}
     ok whenever {fine}

Logic programming-based formulation:
*/
 
happens(correct,3).
initiation(ok,T) :- happens(correct,T), true.
ram(holds(fine,T)) :- holds(good,T).
ram(holds(good,T)) :- holds(ok,T).
ram(holds(ok,T)) :- holds(fine,T).


%Shouldn't be able to infer: sceptical([holds(fine,2)]).
%Should be able to infer: credulous([holds(fine,2)]).
%Should be able to infer: sceptical([holds(fine,4)]).
%Should be able to infer: credulous([holds(fine,4)]).
%Shouldn't be able to infer: sceptical([neg(holds(fine,2))]).
%Should be able to infer: credulous([neg(holds(fine,2))]).
%Shouldn't be able to infer: sceptical([neg(holds(fine,4))]).
%Shouldn't be able to infer: credulous([neg(holds(fine,4))]).

