deonticProver 2.0

`Examples`

Syntax for formulae

Phi ::= a,b,c,... | false | true | neg Phi | Phi and Phi| Phi or Phi | Phi -> Phi | Op(Phi, Phi)
	       with a,b,c,... atoms and op an operator

Syntax for factual assumptions

a1 and a2 and ... and aN -> b1 or ... or bM
		 with a1, ..., aN, b1, ..., bM atoms

Syntax for deontic assumptions

op(phi,psi) | norm:op(phi,psi) | per(op,phi,psi) | norm:per(op,phi,psi)
		 with op an operator, norm an atom, and phi,psi propositional

Syntax for superiority relation

norm1 beats norm2 with norm1, norm2 atoms

Syntax for operator definitions

(op,type) with op the operator you want to define and
		type one of obl or for

Syntax for operator inclusions

op1 -> op2 with op1 and op2 operators

Syntax for operator conflicts

confl(op1,op2) with op1,op2 operators

Syntax for nontrivial operators

op with op operator

Main examples from the article.

The asparagus example
Deontic assumptions:
obl(neg eat_with_fingers, true), obl(eat_with_fingers, asparagus), obl(neg asparagus, true).
Operators: (obl,obl).
Operator conflicts: confl(obl,obl).
Possible questions: obl(neg asparagus, true) or obl(eat_with_fingers, asparagus) or neg obl(neg eat_with_fingers, asparagus).

This example illustrates that more specific deontic assumptions like the obligation to eat with your fingers if asparagus is served override more general conflicting ones like the obligation not to eat with your fingers in general, but not more general nonconflicting ones like the general obligation not to serve asparagus.

The extended asparagus example
Deontic assumptions:

obl(neg eat_with_fingers, true), obl(eat_with_fingers, asparagus), obl(neg asparagus, true), obl(neg eat_with_fingers, grandparents), per(eat_with_fingers, grandparents and asparagus)

.
Operators: (obl,obl), (per,obl).
Operator conflicts: confl(obl,obl), confl(obl,per).
Possible question: obl(eat_with_fingers, asparagus and grandparents).

This is an extension of the asparagus example above, illustrating that more specific permissions, like the permission to eat asparagus with your fingers at your grandparents', can have the effect of reinstating more general obligations, like the obligation to eat asparagus with your fingers. Removing the permission from the deontic assumptions results in an unresolvable conflict between the obligation to eat asparagus with your fingers and the obligation to not eat with your fingers at your grandparents', hence in the situation where you are served asparagus at your grandparents' neither the obligation to eat with your fingers, nor the one not to do so can be derived.

The Drowning Twins
Factual assumptions:
save_twin_1 and save_twin_2 -> false.
Deontic assumptions:
obl(save_twin_1, reachable_twin_1), obl(save_twin_2, reachable_twin_2).
Operators: (obl,obl).
Operator conflicts: confl(obl,obl).
Possible questions are obl(save_twin_1, reachable_twin_1 and reachable_twin_2) or obl(save_twin_1 or save_twin_2, reachable_twin_1 and reachable_twin_2).

This is the standard Drowning Twins example, where two identical twins are both drowning in a pool, and it is not possible to reach both of them in time to save them. The example illustrate that that the system satisfies the disjunctive solution: While it is not possible to decide which of the twins to save, it is at least derivable that one should save the first or the second.

Must-ought-should
Factual assumptions:
help_friend -> murder.
Deontic assumptions:
must(neg murder, true), ought(help_friend, true)
Operators: (must,obl), (ought,obl), (should,obl)
Operator inclusions: must -> ought, must -> should, ought -> should
Operator conflicts: confl(must,must)
Nontrivial operators: ought
Possible questions are must(neg murder, true), or ought(neg murder, true), or ought(murder,true).

This example illustrates inclusions between operators with different properties. While the D axiom neg (must(p,q) and must(neg p,q)) and the P axiom neg must(false,q) are both derivable for the operator must, only the P axiom is derivable for the operator ought, and neither is derivable for should.

The Order Puzzle
Deontic assumptions:
1:obl(neg open_window, heating), 2:obl(open_window,true), 3:obl(heating,true)
Superiority relation:
1 beats 2, 2 beats 3
Operators: (obl,obl)
Operator conflicts: confl(obl,obl)
Possible questions are obl(heating, open_window and neg heating), or obl(neg open_window, open_window and neg heating).

This example illustrates that deontic detachment does not hold for the base logic MD. In particular, there is no aggregation of priorities along chains of conditional obligations, which could make the obligation to open the window overrule the one to turn on the heating, hence the latter is derivable. Adding the deontic assumption obl(neg heating, open_window) would prevent the derivation of the obligation to turn on the heating given the window is open, but using the specificity mechanism instead of the priorities.

Permissions as exceptions 1
Deontic assumptions:
for(parking, true), per(parking,permit).
Operators: (for,for), (per,obl).
Operator conlicts: confl(for,for), confl(for,per).
Possible questions are for(parking, true) and for(parking, lazy) or for(parking, permit) or for(parking, permit and lazy).

This example illustrates how permissions can be modelled as exceptions to other operators, in this case to the prohibition operator for. We could also add other operators, e.g., an obligation type operator (obl,obl) with the additional deontic assumption obl(neg parking, true) and have the permission act as exception to this operator as well by adding the operator conflict confl(obl,per).

Permissions as exceptions 2
Factual assumptions:
steal_food -> steal, steal and respect_others_property -> false.
Deontic assumptions:
for(steal, true), obl(respect_others_property, true), per(steal_food, starving).
Operators: (for,for), (obl,obl), (per,obl).
Operator conlicts: confl(for,for), confl(obl,obl), confl(for,per), confl(obl,per).
Possible questions are for(steal_food, true) and obl(neg steal_food, lazy) or for(steal_food, starving) or obl(neg steal_food, starving) or for(steal and neg steal_food, starving).

This example extends the previous one and illustrates how permissions can be modelled as exceptions to several other operators, in this case to the prohibition operator for and the obligation operator obl. While the permission to steal food when you are starving overrules the general prohibition to steal and the general obligation to respect others' property in case one is starving, we can still derive that it is forbidden to steal anything which is not food in case you are starving.

Sanctions and violations
Deontic assumptions:
sanc(parking, true), viol(parking, true), per_viol(parking, permit), per_sanc(parking, fine_paid).
Operators: (viol,for), (sanc,for), (per_viol,obl), (per_sanc,obl).
Operator inclusions: sanc -> viol.
Operator conlicts: confl(viol,viol), confl(viol,per_viol), confl(sanc,per_sanc).
Possible questions are sanc(parking, true) and viol(parking, true) and viol(parking, fine_paid) or sanc(parking, fine_paid) or sanc(parking, permit) or viol(parking, permit).

This example illustrates how to model sanctions and violations using two operators sanc and viol. In particular, permissions-as-exceptions to the violation operator also overrule the sanction operator, but not vice versa. In particular, it is possible to violate the prohibition to park without further sanction in case the fine was paid.

The fence example
Factual assumptions:
white_fence -> fence.
Deontic assumptions:
viol(fence, true), sanc(fence, true), per_viol(fence, at_the_sea), per_sanc(white_fence, fence).
Operators: (viol,for), (sanc,for), (per_viol,obl), (per_sanc,obl).
Operator inclusions: sanc -> viol.
Operator conlicts: confl(viol,viol), confl(viol,per_viol), confl(sanc,per_sanc).
Possible questions are viol(white_fence, fence) or sanc(white_fence, fence) or viol(fence, at_the_sea) or sanc(fence,fence) or sanc(fence and neg white_fence,fence).

This example illustrates how to model certain aspects of contrary-to-duty reasoning using the two operators viol for the primary prohibition and sanc for the secondary one. The mechanism is as in the previous example in that exceptions to the primary prohibition, like the permission to have a fence at the sea, overrule both the primary and secondary norm, while the contrary-to-duty statement "If there is a fence, it must be a white fence" is modelled as an exception to the secondary norm and hence does not overrule the primary norm. Note that since here we take permissions to be upwards monotone, i.e., of obligation type, we do not have free-choice-permission. In particular, this means that we cannot derive the secondary prohibition sanc(fence,fence), because having a fence does not in all cases violate the secondary norm. However, we can derive sanc(fence and neg white_fence), since having a non-white fence is not covered by the exception.

The Kantian Witness Protection Agent
The factual assumptions are given by
protect_witness -> lie.
The deontic assumptions are given by
kant:for(lie, true), law:obl(protect_witness, killer_asks).
Apart from the empty superiority relation, possible relations are given by
kant beats law or law beats kant.
Operators: (for,for), (obl,obl)
Operator conflicts: confl(obl,obl), confl(for,for), confl(obl,for).
Possible questions are obl(lie, killer_asks) or for(lie, killer_asks).

This example illustrates how the superiority relation can decide conflicts between norms from different sources. The setting is that a witness protection agent adhering to Kantian philosophy is asked by a killer about the location of the witness, and is torn between the general Kantian prohibition to lie and the more specific obligation by law to protect the witness in case the killer comes asking.

The Self-preserving Kantian Witness Protection Agent
The factual assumptions are given by
protect_witness -> lie, lie and save_yourself -> false.
The deontic assumptions are given by
kant:for(lie, true), law:obl(protect_witness, killer_asks), common_sense:obl(save_yourself, true).
Apart from the empty superiority relation, possible relations are given by
kant beats law, law beats common_sense, common_sense beats kant or law beats kant, kant beats common_sense, common_sense beats law.
Operators: (for,for), (obl,obl)
Operator conflicts: confl(obl,obl), confl(for,for), confl(obl,for).
Possible questions again are obl(lie, killer_asks) or for(lie, killer_asks).

This example extends the previous one with a third obligation rooted in common sense. The additional assumption is that the killer would notice that the agent is lying and kill both the witness and the agent. The superiority relation could have many different forms, the two suggested ones are interesting in that they show that the relation may contain cycles of length three.

Examples from Mimamsa reasoning.

Chariot makers and Agnihotra
The factual assumptions are given by


	      chariotmaker -> sudra, sudra and member_higher_caste -> false

.
The deontic assumptions are given by


	      obl(agnihotra,true), obl(neg agnihotra, neg member_higher_caste), obl(agnihotra, chariotmaker)

.
Operators: (obl,obl).
Operator conflicts: confl(obl,obl).
Possible questions are obl(agnihotra,sudra) or obl(neg agnihotra, teacher and sudra).

This example illustrates the use of the specificity principle in Mimamsa reasoning: In general one should perform the agnihotra ritual; but in the more specific case where one is not a member of the higher castes one should refrain from doing so; yet in the even more specific case where one is a chariotmaker, one again should perform the ritual.

Hierarchie between sruti and smrti texts 1
The deontic assumptions are given by


		sruti:obl(agnihotra, caste_1 or caste_2 or caste_3), smrti:for(agnihotra, caste_3 or caste_4)

.
The superiority relation is given by


		sruti beats smrti

.
Operators: (obl,obl), (for,for).
Operator conflicts: confl(obl,obl), confl(obl,for), confl(for,for).
Possible questions are obl(agnihotra, caste_3), for(agnihotra, caste_3), or for(agnihotra, caste_4).

This example illustrates the use of a superiority relation between norms. Without such a relation the reasoning would be skeptical, and the system would be able to derive neither that it is obligatory to perform the Agnihotra ritual given one is a member of the third caste, nor that it is prohibited. With the additional information that Sruti texts (coming directly from the Vedas) have a higher authority than Smrti texts (i.e., commentaries on the Vedas), this tie can be broken.

Hierarchie between sruti and smrti texts 2
The factual assumptions are


		cover_post and touch_post -> false

.
The deontic assumptions are:


		smrti:obl(cover_post, ritual_X), sruti:obl(touch_post, ritual_X)

.
The superiority relation is given by


		sruti beats smrti

.
Operators: (obl,obl).
Operator conflicts: confl(obl,obl).
Possible questions are obl(neg cover_post, ritual_X) or obl(cover_post or touch_post, ritual_X) while varying the superiority relation.

This example again illustrates the use of a superiority relation between norms. Again, without information on whether the obligation to touch a certain post during a particular ritual or the one to cover the post completely with cloth (therefore making it impossible to touch it) takes precedence, the system cannot conclude either. The additional information that one of the obligations comes from the Sruti text, the other one from the Smrti ones, and that Sruti texts overrule Smrti texts breaks the tie.

Some standard paradoxa of deontic logic.

Good Samaritan Paradox
The deontic assumptions are given by


		  obl(help_Smith, mugged_Smith), for(mugged_Smith, true)

.
Operators: (obl,obl), (for,for).
Operator conflicts: confl(obl,obl), confl(obl,for), confl(for,for).
Possible questions: obl(mugged_Smith, mugged_Smith) or for(mugged_Smith, mugged_Smith) and obl(help_Smith, mugged_Smith).

This is the standard Good Samaritan Paradox, where the assumptions are that one should help Smith in case he is mugged, and that he should not be mugged in the first place. In Standard Deontic Logic it is possible from the first assumptions to derive that Smith should be mugged. In our setting this would correspond to obl(mugged_Smith, mugged_Smith), which is not derivable. The fact that this is not derivable here stems from the logic using a dyadic operator to implement obligations, which avoid the inference from "help Smith who is mugged" to "Smith is mugged".

Sartre's dilemma
The factual assumptions are given by
care_for_mother and join_resistance -> false.
The deontic assumptions are given by
family:obl(care_for_mother, mother_depends_on_you), vengeance:obl(join_resistance, brother_was_killed).
Apart from the empty superiority relation, possible relations could be given by family beats vengeance or vengeance beats family.
Operators: (obl,obl).
Operator conflicts: confl(obl,obl).
Possible questions are obl(join_resistance, mother_depends_on_you and brother_was_killed) or obl(neg join_resistance, mother_depends_on_you and brother_was_killed).

This is the standard Sartre's dilemma, where a young French person is torn between the obligations to care for his mother who depends on him and to join the resistance agains the occupying Nazi force in order to avenge the death of his brother. The tie between the two obligations can be broken by labelling one of the sources of the two obligations superior to the other one.

Sophie's Choice
The factual assumptions are
true -> sacrifice_child_1 or sacrifice_child_2.
The deontic assumptions are
for(sacrifice_child_1, true), for(sacrifice_child_2, true).
Operators: (for,for).
Operator conflicts: confl(for,for).
Possible questions are for(sacrifice_child_1, true) or for(sacrifice_child_1 and sacrifice_child_2, true).

This is the standard analog of the Drowning Twins example in terms of prohibitions: Sophie and her two children are at a concentration camp, and Sophie has to decide which of the two children to sacrifice in order to save the other one. Similarly to the previous example, while the system does not decide which child to sacrifice, it derives that Sophie should not sacrifice both of them.

Chisholm's paradox
The deontic assumptions are
obl(assist_neighbours, true), obl(tell_neighbours, assist_neighbours), obl(neg tell_neighbours, neg assist_neighbours).
Operators: (obl,obl).
Operator conflicts: confl(obl,obl).
Possible questions are obl(assist_neighbours, neg assist_neighbours) and obl(neg tell_neighbours, neg assist_neighbours) or obl(tell_neighbours, true).

This is the standard Chisholm example, where one should go to the assistance of one's neighbours and one should tell them in case one is coming but not otherwise. The counterintuitive inference that one should not help the neighbours if one does not do so, which is possible in Standard Deontic Logic SDL, is avoided mainly due to the use of a dyadic operator for obligations.

`Description`

deonticProver2.0 is a Prolog implementation of a generic theorem prover for Deontic Logic extended with reasoning from factual and deontic assumptions, using the specificity principle and a superiority relation for conflict resolution. It is based on the article Sequent Rules for Reasoning and Conflict Resolution in Conditional Norms (To appear in DEON 2020/2021).

Formulae are built from the grammar

Phi ::= atom | false | true | neg Phi | Phi and Phi | Phi or Phi | Phi -> Phi | Op(Phi, Phi) where atom is any Prolog atom, e.g., p, q, r, ..., murder, murder_gently, ... and Op is the name of an operator in the form of a Prolog atom, e.g., obl, for, must, ought, should, ... 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 deontic formulae, i.e., formulae of the form Op(A,B) with Op an operator, or labelled non-nested deontic formulae, i.e., formulae of the form Norm:Op(A,B) with Norm the name of a norm in the form of a Prolog atom, e.g., law, common_sense, criminal_law, .... In both cases the formulae A and B must not contain any operators. It is possible to give the same label to multiple formulae.

The superiority relation is given as a list of formulae Norm_1 beats Norm_2, where Norm_1 and Norm_2 are labels of deontic assumptions. The effect is that in presence of Norm_1 beats Norm_2 every deontic assumption labelled with Norm_1 is stronger than every deontic assumption labelled with Norm_2. The superiority relation must not contain cycles of length at most two, i.e. it must not contain both Norm_1 beats Norm_2 and Norm_2 beats Norm_1, and it must not contain Norm beats Norm.

The operators are given as a list of operators with associated type (Op,Type), where Op is the name of an operator, and Type is either obl (for obligation type operators) or for (for prohibition type operators). An operator can have only one type. The effect is that in presence of (Op,obl) the axiom Op(A and B,C) -> Op(A,C) is assumed, while in presence of (Op,for) the axiom Op(A,C) -> Op(A and B,C) is assumed.

Operator inclusions are given as a list of formulae Op_1 -> Op_2 with Op_1,Op_2 operators. The effect is that in presence of Op_1 -> Op_2 an inclusion axiom between the two operators is assumed. This has the form Op_1(A,B) -> Op_2(A,B) if the operators have the same type, and Op_1(A,B) -> Op_2(neg A,B) otherwise. The system automatically closes the inclusions under transitivity.

Operator conflicts are given as a list of formulae confl(Op_1,Op_2) with Op_1, Op_2 operators. The two operators can be the same. The effect is that in presence of confl(Op_1,Op_2) the D axiom neg (Op_1(A,B) and Op_2(neg A,B)) is assumed. The system automatically closes the operators under symmetry and the preimage of the inclusion relation, i.e., if Op_1 -> Op_2 and confl(Op_2,Op_3), then the system adds all of confl(Op_1,Op_3), confl(Op_3,Op_2), confl(Op_3,Op_1).

The nontrivial operators are given as a list of operators. The effect is that if Op is in the list of nontrivial operators, then the P axiom neg (Op(false,A) and Op(true,A)) is assumed. This is equivalent to the axiom neg Op(false,A) for obligation type operators and neg (true,A) for prohibition type operators. The system automatically closes the set of nontrivial operators under the preimage of the inclusion relation, i.e., if Op_1 -> Op_2 and Op_2 is in the list of nontrivial operators, then the system also adds Op_1 to the list.

To run the prover, input your data, at the very least your formula and the operators in it with their types, then 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 latex source code and manually split the derivation.

The precursor deonticProver can be found here.

For further information, contact Björn Lellmann. We thank Carlos Olarte for his help in implementing this site.

deonticProver2.0

`Formula to be checked`

`Factual Assumptions`

`Deontic Assumptions`

`Superiority Relation`

`Operators`

`Operator inclusions`

`Operator conflicts`

`Nontrivial operators`

`Examples`

`Description`