Skip to content

Commit cfe8585

Browse files
lex-lexlex-lex
committed
Merge branch 'master' of github.com:lex-lex/Leo-III
2 parents 0c9a2d2 + 94e6ca9 commit cfe8585

18 files changed

+268
-2
lines changed

‎demo/deontic/GDPR.ddl.p

+23
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,23 @@
1+
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
2+
% Example: GDPR in Dyadic deontic logic (Carmo/Jones)
3+
%
4+
% $O(p) corresponds to OB (obligatory) p
5+
% $O(p/q) corresponds to 'it ought to be p given q'
6+
% ...
7+
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
8+
9+
%--- It is obligatory to process data lawfully
10+
ddl(a1, axiom, $O(processDataLawfully)).
11+
12+
%--- If data is not processed lawfully it has to be erased
13+
ddl(a2, axiom, (~processDataLawfully) => $O(eraseData)).
14+
15+
%--- Data is actually not processed lawfully
16+
ddl(situationalAx, localAxiom, ~processDataLawfully).
17+
18+
%--- Is it obligatory to delete the data?
19+
ddl(c1, conjecture, $O(eraseData)).
20+
21+
%%% Commented out
22+
%--- Consistency check: Is it obligatory to kill the boss?
23+
%ddl(c3, conjecture, $O(kill)).

‎demo/deontic/GDPR.modal.p

+36
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,36 @@
1+
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
2+
% Example: CTD in standard deontic logic (GDPR)
3+
%
4+
% $box corresponds to OB (obligatory)
5+
% $dia corresponds to PE (permissible)
6+
% ...
7+
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
8+
9+
%--- logic specification for SDL
10+
thf(spec, logic, ($modal := [
11+
$constants := $rigid,
12+
$quantification := $constant,
13+
$consequence := [$global,
14+
situationalAxiom := $local],
15+
$modalities := $modal_system_D ] ) ).
16+
17+
%--- declare atomic propositions
18+
thf(type1, type, processDataLawfully: $o).
19+
thf(type2, type, eraseData: $o).
20+
21+
%--- It is obligatory to process data lawfully
22+
thf(ax1, axiom, $box @ processDataLawfully).
23+
24+
%--- If data is not processed lawfully it has to be erased
25+
thf(ax2, axiom, (~ (processDataLawfully))
26+
=> ($box @ eraseData)).
27+
28+
%--- Lawfully processed data must be kept
29+
thf(ax3, axiom, $box @ (processDataLawfully => ~(eraseData))).
30+
31+
%--- Data is actually not processed lawfully
32+
thf(situationalAxiom, axiom, ~ (processDataLawfully)).
33+
34+
%--- Is it obligatory to delete the data?
35+
thf(c, conjecture, $box @ eraseData).
36+

‎demo/deontic/leo3nitpick

+3
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,3 @@
1+
#!/bin/bash
2+
3+
leo3 $@ --atp nitpick --atp-timeout nitpick=60

‎demo/ho/choice_swap.p

+8
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,8 @@
1+
%-- For any X,Y:i, there is a function swapping X and Y
2+
thf(ifi,conjecture,(
3+
! [X: $i,Y: $i] :
4+
? [F: $i > $i] :
5+
( ( ( F @ X )
6+
= Y )
7+
& ( ( F @ Y )
8+
= X ) ) )).

‎demo/ho/inj_cantor.p

+6
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,6 @@
1+
2+
%-- There is no injection from a power set to its underlying set.
3+
thf(inj_cantor, conjecture, (~ ( ? [F: ($i > $o) > $i] : (
4+
! [X: $i > $o,Y:$i > $o]:
5+
(((F @ X) = (F @ Y)) => (X = Y))
6+
) ))).

‎demo/ho/sur_cantor.p

+9
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,9 @@
1+
2+
%-- There is no surjective function from a set to its power set.
3+
thf(sur_cantor, conjecture, (~ ( ? [F: $i > ($i > $o)] : (
4+
! [Y: $i > $o] :
5+
? [X: $i] : (
6+
(F @ X) = Y
7+
)
8+
) ))).
9+

‎demo/modal.zip

4.36 KB
Binary file not shown.

‎demo/modal/ex1_semantics.p

+14
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,14 @@
1+
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
2+
% Example 1: Basic modal reasoning
3+
%
4+
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
5+
6+
%--- logic specification
7+
thf(spec, logic, ( $modal := [
8+
$constants := $rigid,
9+
$quantification := $constant,
10+
$consequence := $global,
11+
$modalities := $modal_system_S5 ] )).
12+
13+
%--- does ϕ → □◇ϕ hold?
14+
thf(mysterious, conjecture, ![A:$o]: (A => ($box @ ($dia @ A))) ).

‎demo/modal/ex1_semantics_ho.p

+19
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,19 @@
1+
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
2+
% Example 1b: Basic modal reasoning
3+
%
4+
% (corollary from Beckers postulate)
5+
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
6+
7+
%--- logic specification
8+
thf(spec, logic, ( $modal := [
9+
$constants := $rigid,
10+
$quantification := $constant,
11+
$consequence := $global,
12+
$modalities := $modal_system_S5 ] )).
13+
14+
%--- Does there ∃g s.t. ◇□p(f(x)) → □p(g(x)) holds?
15+
thf(1,conjecture,(
16+
! [P: ( $i > $o ),F: ( $i > $i ),X: $i] :
17+
? [G: ( $i > $i )] :
18+
( ( $dia @ ( $box @ ( P @ ( F @ X ) ) ) )
19+
=> ( $box @ ( P @ ( G @ X ) ) ) ) )).

‎demo/modal/ex2_quantification_bf.p

+20
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,20 @@
1+
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
2+
% Example 2: Quantification semantics
3+
%
4+
% see also QMLTP SYM001+1
5+
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
6+
7+
%--- logic specification
8+
thf(spec, logic, ($modal := [
9+
$constants := $rigid,
10+
$quantification := $decreasing,
11+
$consequence := $global,
12+
$modalities := $modal_system_K ] ) ).
13+
14+
%--- Specify an uninterpreted predicate symbol f
15+
thf(f_type, type, f: ($i > $o)).
16+
17+
%--- Does BF: (∀x.□f(x)) → □∀x.f(x) hold?
18+
thf(barcan_formula, conjecture, (
19+
(![X:$i]: ( $box @ (f @ X) ))
20+
=> ($box @ ( ![X: $i]: ( f @ X ) )) ) ).

‎demo/modal/ex2_quantification_cbf.p

+20
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,20 @@
1+
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
2+
% Example 2b: Quantification semantics
3+
%
4+
% see also QMLTP SYM002+1
5+
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
6+
7+
%--- logic specification
8+
thf(spec, logic, ($modal := [
9+
$constants := $rigid,
10+
$quantification := $cumulative,
11+
$consequence := $global,
12+
$modalities := $modal_system_K ] ) ).
13+
14+
%--- Specify an uninterpreted predicate symbol f
15+
thf(f_type, type, f: ($i > $o)).
16+
17+
%--- Does CBF: (□∀x.f(x)) → ∀x.□f(x) hold?
18+
thf(barcan_formula, conjecture, (
19+
($box @ ( ![X: $i]: ( f @ X ) ))
20+
=> (![X:$i]: ( $box @ (f @ X) )) ) ).

‎demo/modal/ex3_consequence.p

+19
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,19 @@
1+
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
2+
% Example 3: Consequence
3+
%
4+
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
5+
6+
%--- logic specification
7+
thf(spec, logic, ($modal := [
8+
$constants := $rigid,
9+
$quantification := $constant,
10+
$consequence := $local,
11+
$modalities := $modal_system_K ] ) ).
12+
13+
%--- a is some formula
14+
thf(a_type, type, a:$o).
15+
%--- a is valid
16+
thf(ax1, axiom, a).
17+
18+
%--- Does □a hold?
19+
thf(c, conjecture, ($box @ a)).

‎demo/modal/ex4_countermodels.p

+19
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,19 @@
1+
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
2+
% Example 4: Counter-models
3+
%
4+
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
5+
6+
%--- logic specification
7+
thf(spec, logic, ($modal := [
8+
$constants := $rigid,
9+
$quantification := $constant,
10+
$consequence := $global,
11+
$modalities := $modal_system_K ] ) ).
12+
13+
%--- a is some formula
14+
thf(a_type, type, a:$o).
15+
%--- □a is valid
16+
thf(ax1, axiom, $box @ a).
17+
18+
%--- Does a hold?
19+
thf(c, conjecture, a).

‎demo/modal/ex5_multimodal_wisemen.p

+43
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,43 @@
1+
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
2+
% Example 5: Wise men puzzle
3+
%
4+
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
5+
6+
%--- logic specification
7+
thf(wise_men_puzzle_semantics, logic , ( $modal := [
8+
$constants := $rigid, $quantification := $varying,
9+
$consequence := $global, $modalities := $modal_system_S5] )).
10+
11+
%--- $i type models the agents's hats
12+
thf(agent_a, type, (a: $i)).
13+
thf(agent_b, type, (b: $i)).
14+
thf(agent_c, type, (c: $i)).
15+
16+
%--- Property of an agent's hat: ws represents "having a white spot"
17+
thf(white_spot, type, (ws: ($i>$o))).
18+
19+
%--- Common knowledge: At least one agent has a white spot
20+
thf(axiom_1, axiom, ($box_int @ 0 @ ((ws @ a) | (ws @ b) | (ws @ c)))).
21+
22+
%--- If one agent has a white spot all other agents can see this
23+
thf(axiom_2ab, axiom, ($box_int @ 0 @ ((ws @ a) => ($box_int @ 2 @ (ws @ a))))).
24+
thf(axiom_2ac, axiom, ($box_int @ 0 @ ((ws @ a) => ($box_int @ 3 @ (ws @ a))))).
25+
thf(axiom_2ba, axiom, ($box_int @ 0 @ ((ws @ b) => ($box_int @ 1 @ (ws @ b))))).
26+
thf(axiom_2bc, axiom, ($box_int @ 0 @ ((ws @ b) => ($box_int @ 3 @ (ws @ b))))).
27+
thf(axiom_2ca, axiom, ($box_int @ 0 @ ((ws @ c) => ($box_int @ 1 @ (ws @ c))))).
28+
thf(axiom_2cb, axiom, ($box_int @ 0 @ ((ws @ c) => ($box_int @ 2 @ (ws @ c))))).
29+
30+
%--- If one agent has a black spot all other agents can see this
31+
thf(axiom_3ab, axiom, ($box_int @ 0 @ ((~(ws @ a)) => ($box_int @ 2 @ (~(ws @ a)))))).
32+
thf(axiom_3ac, axiom, ($box_int @ 0 @ ((~(ws @ a)) => ($box_int @ 3 @ (~(ws @ a)))))).
33+
thf(axiom_3ba, axiom, ($box_int @ 0 @ ((~(ws @ b)) => ($box_int @ 1 @ (~(ws @ b)))))).
34+
thf(axiom_3bc, axiom, ($box_int @ 0 @ ((~(ws @ b)) => ($box_int @ 3 @ (~(ws @ b)))))).
35+
thf(axiom_3ca, axiom, ($box_int @ 0 @ ((~(ws @ c)) => ($box_int @ 1 @ (~(ws @ c)))))).
36+
thf(axiom_3cb, axiom, ($box_int @ 0 @ ((~(ws @ c)) => ($box_int @ 2 @ (~(ws @ c)))))).
37+
38+
%--- Agents 1 and 2 do not know their hat color
39+
thf(axiom_9, axiom, ($box_int @ 0 @ (~($box_int @ 1 @ (ws @ a))))).
40+
thf(axiom_10, axiom, ($box_int @ 0 @ (~($box_int @ 2 @ (ws @ b))))).
41+
42+
%--- Agent 3 can deduce the color of his hat (white spot)
43+
thf(con, conjecture, ($box_int @ 3 @ (ws @ c))).

‎demo/modal/findCounterModel

+3
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,3 @@
1+
#!/bin/bash
2+
embedModal -i $1 -o /tmp/out.p 2>/dev/null
3+
isabelle tptp_nitpick 60 /tmp/out.p

‎demo/modal/leo3nitpick

+3
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,3 @@
1+
#!/bin/bash
2+
3+
leo3 $@ --atp nitpick --atp-timeout nitpick=60

‎demo/poly/sur_cantor_th1.p

+7
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,7 @@
1+
thf(sur_cantor, conjecture,
2+
( ! [T: $tType]: (~ ( ? [F: T > (T > $o)] : (
3+
! [Y: T > $o] :
4+
? [X: T] : (
5+
(F @ X) = Y
6+
)
7+
) )))).

‎src/main/scala/leo/modules/prover/Control.scala

+16-2
Original file line numberDiff line numberDiff line change
@@ -195,7 +195,8 @@ package inferenceControl {
195195
while (clCNF.hasNext) {
196196
val next = clCNF.next()
197197
// val simplified = Control.cheapSimp(Control.liftEq(next))
198-
val simplified = Control.liftEq(next)
198+
val lifted = Control.liftEq(next)
199+
val simplified = SimplificationControl.cheapSimp2(lifted)
199200
if (FullCNF.canApply(simplified.cl)) {
200201
temp += simplified
201202
} else {
@@ -1930,7 +1931,20 @@ package inferenceControl {
19301931
cl
19311932
}
19321933

1933-
1934+
final def cheapSimp2(cl: AnnotatedClause)(implicit state: State[AnnotatedClause]): AnnotatedClause = {
1935+
implicit val sig: Signature = state.signature
1936+
Out.trace(s"[Simp2] Processing ${cl.pretty(sig)}")
1937+
// if (isPropSet(ClauseAnnotation.PropShallowSimplified, cl.properties) || isPropSet(ClauseAnnotation.PropFullySimplified, cl.properties))
1938+
// cl
1939+
// else {
1940+
val simpResult = Simp(cl.cl)
1941+
val result0 = if (simpResult == cl.cl) cl
1942+
else AnnotatedClause(simpResult, InferredFrom(Simp, cl), addProp(ClauseAnnotation.PropShallowSimplified,cl.properties))
1943+
val result = result0
1944+
Out.finest(s"[Simp] Result: ${result.pretty(sig)}")
1945+
result
1946+
// }
1947+
}
19341948
final def cheapSimp(cl: AnnotatedClause)(implicit state: State[AnnotatedClause]): AnnotatedClause = {
19351949
implicit val sig: Signature = state.signature
19361950
Out.trace(s"[Simp] Processing ${cl.pretty(sig)}")

0 commit comments

Comments
 (0)