-
Notifications
You must be signed in to change notification settings - Fork 2
/
Copy pathdeontic-rules.lisp
66 lines (47 loc) · 2.25 KB
/
deontic-rules.lisp
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
;;;; Reasoning rules for deontic opeators: Obl, Forb, Perm and Facult
;;;; Author: Chun Tian (binghe)
;;;;
;;;; Based on `An Axiomatisation for Deontic Reasoning'
;;;; (Sec 17.4 of `Legal Reasoning: A Cognitive Approach to the Law', by Giovanni Sartor)
(in-package "OSCAR")
(def-forwards-reason FON1
:forwards-premises "(Forb A)" :conclusions "(Obl ~A)" :variables A)
(def-forwards-reason FON2
:forwards-premises "(Obl ~A)" :conclusions "(Forb A)" :variables A)
(def-forwards-reason OP
:forwards-premises "(Obl A)" :conclusions "(Perm A)" :variables A)
(def-forwards-reason PNF1
:forwards-premises "(Forb A)" :conclusions "~(Perm A)" :variables A)
(def-forwards-reason PNF2
:forwards-premises "~(Perm A)" :conclusions "(Forb A)" :variables A)
(def-forwards-reason JO
:forwards-premises "(Obl A)" "(Obl B)" :conclusions "(Obl A & B)"
:variables A B :defeasible? t)
(def-backwards-reason i-FON1
:backwards-premises "(Forb A)" :conclusions "(Obl ~A)" :variables A)
(def-backwards-reason i-FON2
:backwards-premises "(Obl ~A)" :conclusions "(Forb A)" :variables A)
(def-backwards-reason i-OP
:backwards-premises "(Obl A)" :conclusions "(Perm A)" :variables A)
(def-backwards-reason i-PNF1
:backwards-premises "(Forb A)" :conclusions "~(Perm A)" :variables A)
(def-backwards-reason i-PNF2
:backwards-premises "~(Perm A)" :conclusions "(Forb A)" :variables A)
(def-backwards-reason i-JO
:backwards-premises "(Obl A)" "(Obl B)" :conclusions "(Obl A & B)"
:variables A B :defeasible? t)
;;; The support of Facultativeness
(def-forwards-reason FP1
:forwards-premises "(Fault A)" :conclusions "(Perm A) & (Perm ~A)" :variables A)
(def-forwards-reason FP2
:forwards-premises "(Perm A)" "(Perm ~A)" :conclusions "(Fault A)" :variables A)
(def-backwards-reason i-FP1
:backwards-premises "(Fault A)" :conclusions "(Perm A) & (Perm ~A)" :variables A)
(def-backwards-reason i-FP2
:backwards-premises "(Perm A)" "(Perm ~A)" :conclusions "(Fault A)" :variables A)
(setq *forwards-logical-reasons*
(nconc *forwards-logical-reasons*
(list FON1 FON2 OP PNF1 PNF2 JO FP1 FP2)))
(setq *backwards-logical-reasons*
(nconc *backwards-logical-reasons*
(list i-FON1 i-FON2 i-OP i-PNF1 i-PNF2 i-JO i-FP1 i-FP2)))