:- module(proof_tree, [export/0, export/1, view/0, view/1]). /** Proof tree example */ :- use_module(library(apply)). :- use_module(library(yall)). :- use_module(library(gv)). export :- proof(Proof), export(Proof). export(Proof) :- gv_export('proof_tree.svg', {Proof}/[Out]>>export_proof_(Out, Proof), [directed(true)]). proof(t(rdfs(3), ∈(class,class), [t(axiom(rdfs), range(range,class), []), t(axiom(rdfs), range(⊆,class), [])])). view :- proof(Proof), view(Proof). view(Proof) :- gv_view({Proof}/[Out]>>export_proof_(Out, Proof), [directed(true)]). export_proof_(Out, Proof) :- Proof = t(Rule,Concl,SubProofs), dot_node(Out, Concl), dot_node(Out, Proof, [label(Rule)]), dot_arc(Out, Concl, Proof), maplist(export_subproof_(Out, Proof), SubProofs). export_subproof_(Out, Proof, SubProof) :- SubProof = t(_,Prem,_), dot_node(Out, Prem), dot_arc(Out, Proof, Prem), export_proof_(Out, SubProof).