Chariot makers and Agnihotra
The factual assumptions are given by
chmk -> sudra, sudra and mhk -> false
The deontic assumptions are given by
obl(agn,true), obl(neg agn, neg mhk), obl(agn, chmk)
Possible questions are obl(agn,sudra) or obl(neg agn, teacher and sudra).
K
?(5, p + q) , ?(4, r + t), !(1, p ^ * t ^)
?(1, q) && ?(1, p) && !(1, p ^ * q ^)
?(1, p * q ^) && ?(1, p ^) && !(1, q)
K + 4
?(1, p), !(1, !(1, p ^))
?(3, p + q), !(2, !(1, p ^ ))
?(5, p) , ?(4, q), !(2, !(1, p ^ * q ^))
?(3, p ^) , !(2, !(1, p))
K + D
?(1,p) , ?(1, p ^)
?(2,?(1, p)) , ?(2, !(1, p ^))
?(1, ?(1, p)) && ?(1, ?(1, p ^))
K + T
?(1,p), p ^
K + D + 4
?(2, p) && ?(2, ?(1, p ^))
?(3, ?(2, p)) && ?(2, ?(1, p ^))
Phi ::= atom | false | true | neg Phi | Phi and Phi | Phi or Phi | Phi -> Phi | obl(Phi, Phi) | rec(Phi, Phi)
where atom is any Prolog atom, e.g., p,q,r,...,kill,syena,harm,...
The usual conventions about binding strength of the connectives apply, i.e.,
and binds stronger than or binds stronger than ->.
Facts are lists of clauses, i.e., lists of formulae of the form atom1 and atom2 and ... -> atomn or atomn+1 or ...
Deontic assumptions are lists of non-nested obligation formulae, i.e., lists of formulae of the form obl(A,B) or rec(A,B), where the formulae A and B do not contain the obl and rec operators.
To run the prover, input your formula, your factual assumptions, and your deontic assumptions, then and hit 'Prove'. If the formula is derivable, the derivation is displayed automatically. You might need to zoom in a bit for large derivations.
NOTE: In some cases the derivations might become too large for TeX
to handle (if they are more than about 19 feet). In these cases no
pdf output is produced. However, you may still download the
source code, run the prover locally and manually split the derivation.
The prover implements backwards proof search in the dyadic version
of non-monotone modal logic MD for the obligation operator
obl(.,.) given by the rules and axioms
(A -> B) / obl(A,C) -> obl(B,C)
(B -> C) and (C -> B) / obl(A,B) -> obl(A,C)
neg (obl(A,B) and obl(neg A, B))
as well as the dyadic version of non-monotone modal logic
MP for the recommendation operator rec(.,.), given by the
following rules and axiom:
(A -> B) / rec(A,C) -> rec(B,C)
(B -> C) and (C -> B) / rec(A,B) -> rec(A,C)
neg rec(false,A)
It further implements
the reading of the specificity principle in the step from
deontic assumptions to provable formulae from the article Resolving
conflicting obligations in Mimamsa: A sequent-based
approach. The calculi are implemented in their rendering in
the framework of linear nested sequents, following the
methods of decomposing sequent rules into linear nested sequent
rules from this paper.
The source code can be downloaded here
and is available on github here.
For further information, contact Björn Lellmann. We thank Carlos Olarte for his help in implementing this site.