SWISH -- SWI-Prolog for SHaring

:- use_module(library(scasp)).
:- style_check(-discontiguous).
:- style_check(-singleton).
:- set_prolog_flag(scasp_unknown, fail).

#pred bird(X) :: '@(X) is a bird'.
#pred according_to(R,bird(X)) :: 'according to @(R), @(X) is a bird'.
#pred legally_holds(_,bird(X)) :: 'it legally holds that @(X) is a bird'.
#pred penguin(X) :: '@(X) is a penguin'.
#pred according_to(R,penguin(X)) :: 'according to @(R), @(X) is a penguin'.
#pred legally_holds(_,penguin(X)) :: 'it legally holds that @(X) is a penguin'.
bird(X) :-
penguin(X).

#pred thing(X) :: '@(X) is a thing'.
#pred according_to(R,thing(X)) :: 'according to @(R), @(X) is a thing'.
#pred legally_holds(_,thing(X)) :: 'it legally holds that @(X) is a thing'.
#pred flies(Y,X) :: 'it is @(X) that @(Y) flies'.
#pred according_to(R,flies(Y,X)) :: 'according to @(R), it is @(X) that @(Y) flies'.
#pred legally_holds(_,flies(Y,X)) :: 'it legally holds that it is @(X) that @(Y) flies'.

according_to( ba__2_end,flies(A,true)) :-
bird(A).

overrules(ba__3_end,ba__2_end).
opposes(  flies(A,true),  flies(A,false)).
opposes(  flies(A,false),  flies(A,true)).

according_to( ba__3_end,flies(A,false)) :-
penguin(A).

penguin(tweety).

#pred overrules(R1,R2) :: 'the conclusion in @(R1) overrules the conclusion in @(R2)'.
#pred opposes(C1,C2) :: 'the conclusion @(C1) opposes the conclusion @(C2)'.
#pred defeated(R,_) :: 'the conclusion in @(R) is defeated'.
#pred refuted(R,_) :: 'the conclusion in @(R) is refuted'.

refuted(R,C) :-
    opposes(C,OC),
    overrules(OR,R),
    according_to(OR,OC).

defeated(R,C) :-
    refuted(R,C).

legally_holds(R,C) :-
    according_to(R,C),
    not defeated(R,C).

%?- scasp(legally_holds(_,flies(tweety,A)),[tree(Tree)]),with_output_to(string(Human), human_justification_tree(Tree,[])).