Project

General

Profile

Bug #14

Bug #13: Wrong CL result

Strange CL result

Added by Thorsten Wißmann over 3 years ago. Updated over 3 years ago.

Status:
Closed
Priority:
Normal
Assignee:
-
Start date:
05/09/2014
Due date:
% Done:

0%


Description

What would tatl do?

History

#1 Updated by Thorsten Wißmann over 3 years ago

Tatl claims the solution to be satisfiable:

         ----------------------------------------------
         |           TATL : Tableaux for ATL          |
         |          Amelie David - Lab. IBISC         |
         |     23 bd de France -  91037 Evry Cedex    |
         ----------------------------------------------

*
* The formula is satisfiable.
*

*
* Pre-tableau 
**************

P0: ~<<1,3>>X~c/\~<<2,3>>X~~c/\<<1,2,3,4,5>>X(p\/~p)
   Succ: S1
P1: ~~c
   Succ: S6
P2: ~~~c
   Succ: S5
P3: T
   Succ: S4
P4: p\/~p
   Succ: S2 ; S3
S1 (Consistant) : ~<<1,3>>X~c ; ~<<2,3>>X~~c ; ~<<1,3>>X~c/\~<<2,3>>X~~c ; ~<<1,3>>X~c/\~<<2,3>>X~~c/\<<1,2,3,4,5>>X(p\/~p) ; <<1,2,3,4,5>>X(p\/~p)
   Succ: (0,1,0,1,2)(0,1,0,2,1)(0,1,1,1,2)(0,1,1,2,1)(0,1,2,1,1)(0,1,2,2,2)(0,2,0,1,1)(0,2,0,2,2)(0,2,1,1,1)(0,2,1,2,2)(0,2,2,1,2)(0,2,2,2,1)(1,1,0,1,2)(1,1,0,2,1)(1,1,1,1,2)(1,1,1,2,1)(1,1,2,1,1)(1,1,2,2,2)(1,2,0,1,1)(1,2,0,2,2)(1,2,1,1,1)(1,2,1,2,2)(1,2,2,1,2)(1,2,2,2,1)(2,1,0,1,1)(2,1,0,2,2)(2,1,1,1,1)(2,1,1,2,2)(2,1,2,1,2)(2,1,2,2,1)(2,2,0,1,2)(2,2,0,2,1)(2,2,1,1,2)(2,2,1,2,1)(2,2,2,1,1)(2,2,2,2,2)->P1 ; (1,0,0,1,1)(1,0,0,2,2)(1,0,1,1,1)(1,0,1,2,2)(1,0,2,1,2)(1,0,2,2,1)(1,1,0,1,1)(1,1,0,2,2)(1,1,1,1,1)(1,1,1,2,2)(1,1,2,1,2)(1,1,2,2,1)(1,2,0,1,2)(1,2,0,2,1)(1,2,1,1,2)(1,2,1,2,1)(1,2,2,1,1)(1,2,2,2,2)(2,0,0,1,2)(2,0,0,2,1)(2,0,1,1,2)(2,0,1,2,1)(2,0,2,1,1)(2,0,2,2,2)(2,1,0,1,2)(2,1,0,2,1)(2,1,1,1,2)(2,1,1,2,1)(2,1,2,1,1)(2,1,2,2,2)(2,2,0,1,1)(2,2,0,2,2)(2,2,1,1,1)(2,2,1,2,2)(2,2,2,1,2)(2,2,2,2,1)->P2 ; (0,0,0,0,1)(0,0,0,0,2)(0,0,0,1,0)(0,0,0,1,1)(0,0,0,1,2)(0,0,0,2,0)(0,0,0,2,1)(0,0,0,2,2)(0,0,1,0,0)(0,0,1,0,1)(0,0,1,0,2)(0,0,1,1,0)(0,0,1,1,1)(0,0,1,1,2)(0,0,1,2,0)(0,0,1,2,1)(0,0,1,2,2)(0,0,2,0,0)(0,0,2,0,1)(0,0,2,0,2)(0,0,2,1,0)(0,0,2,1,1)(0,0,2,1,2)(0,0,2,2,0)(0,0,2,2,1)(0,0,2,2,2)(0,1,0,0,0)(0,1,0,0,1)(0,1,0,0,2)(0,1,0,1,0)(0,1,0,1,1)(0,1,0,2,0)(0,1,0,2,2)(0,1,1,0,0)(0,1,1,0,1)(0,1,1,0,2)(0,1,1,1,0)(0,1,1,1,1)(0,1,1,2,0)(0,1,1,2,2)(0,1,2,0,0)(0,1,2,0,1)(0,1,2,0,2)(0,1,2,1,0)(0,1,2,1,2)(0,1,2,2,0)(0,1,2,2,1)(0,2,0,0,0)(0,2,0,0,1)(0,2,0,0,2)(0,2,0,1,0)(0,2,0,1,2)(0,2,0,2,0)(0,2,0,2,1)(0,2,1,0,0)(0,2,1,0,1)(0,2,1,0,2)(0,2,1,1,0)(0,2,1,1,2)(0,2,1,2,0)(0,2,1,2,1)(0,2,2,0,0)(0,2,2,0,1)(0,2,2,0,2)(0,2,2,1,0)(0,2,2,1,1)(0,2,2,2,0)(0,2,2,2,2)(1,0,0,0,0)(1,0,0,0,1)(1,0,0,0,2)(1,0,0,1,0)(1,0,0,1,2)(1,0,0,2,0)(1,0,0,2,1)(1,0,1,0,0)(1,0,1,0,1)(1,0,1,0,2)(1,0,1,1,0)(1,0,1,1,2)(1,0,1,2,0)(1,0,1,2,1)(1,0,2,0,0)(1,0,2,0,1)(1,0,2,0,2)(1,0,2,1,0)(1,0,2,1,1)(1,0,2,2,0)(1,0,2,2,2)(1,1,0,0,0)(1,1,0,0,1)(1,1,0,0,2)(1,1,0,1,0)(1,1,0,2,0)(1,1,1,0,0)(1,1,1,0,1)(1,1,1,0,2)(1,1,1,1,0)(1,1,1,2,0)(1,1,2,0,0)(1,1,2,0,1)(1,1,2,0,2)(1,1,2,1,0)(1,1,2,2,0)(1,2,0,0,0)(1,2,0,0,1)(1,2,0,0,2)(1,2,0,1,0)(1,2,0,2,0)(1,2,1,0,0)(1,2,1,0,1)(1,2,1,0,2)(1,2,1,1,0)(1,2,1,2,0)(1,2,2,0,0)(1,2,2,0,1)(1,2,2,0,2)(1,2,2,1,0)(1,2,2,2,0)(2,0,0,0,0)(2,0,0,0,1)(2,0,0,0,2)(2,0,0,1,0)(2,0,0,1,1)(2,0,0,2,0)(2,0,0,2,2)(2,0,1,0,0)(2,0,1,0,1)(2,0,1,0,2)(2,0,1,1,0)(2,0,1,1,1)(2,0,1,2,0)(2,0,1,2,2)(2,0,2,0,0)(2,0,2,0,1)(2,0,2,0,2)(2,0,2,1,0)(2,0,2,1,2)(2,0,2,2,0)(2,0,2,2,1)(2,1,0,0,0)(2,1,0,0,1)(2,1,0,0,2)(2,1,0,1,0)(2,1,0,2,0)(2,1,1,0,0)(2,1,1,0,1)(2,1,1,0,2)(2,1,1,1,0)(2,1,1,2,0)(2,1,2,0,0)(2,1,2,0,1)(2,1,2,0,2)(2,1,2,1,0)(2,1,2,2,0)(2,2,0,0,0)(2,2,0,0,1)(2,2,0,0,2)(2,2,0,1,0)(2,2,0,2,0)(2,2,1,0,0)(2,2,1,0,1)(2,2,1,0,2)(2,2,1,1,0)(2,2,1,2,0)(2,2,2,0,0)(2,2,2,0,1)(2,2,2,0,2)(2,2,2,1,0)(2,2,2,2,0)->P3 ; (0,0,0,0,0)->P4
S2 (Consistant) : p ; p\/~p ; <<1,2,3,4,5>>XT
   Succ: (0,0,0,0,0)->P3
S3 (Consistant) : ~p ; p\/~p ; <<1,2,3,4,5>>XT
   Succ: (0,0,0,0,0)->P3
S4 (Consistant) : T ; <<1,2,3,4,5>>XT
   Succ: (0,0,0,0,0)->P3
S5 (Consistant) : ~c ; ~~~c ; <<1,2,3,4,5>>XT
   Succ: (0,0,0,0,0)->P3
S6 (Consistant) : c ; ~~c ; <<1,2,3,4,5>>XT
   Succ: (0,0,0,0,0)->P3
*
* Tableau 
**********

S1 (Consistant) : ~<<1,3>>X~c ; ~<<2,3>>X~~c ; ~<<1,3>>X~c/\~<<2,3>>X~~c ; ~<<1,3>>X~c/\~<<2,3>>X~~c/\<<1,2,3,4,5>>X(p\/~p) ; <<1,2,3,4,5>>X(p\/~p)
   Succ: (0,0,0,0,0)->S2 ; (0,0,0,0,0)->S3 ; (0,0,0,0,1)(0,0,0,0,2)(0,0,0,1,0)(0,0,0,1,1)(0,0,0,1,2)(0,0,0,2,0)(0,0,0,2,1)(0,0,0,2,2)(0,0,1,0,0)(0,0,1,0,1)(0,0,1,0,2)(0,0,1,1,0)(0,0,1,1,1)(0,0,1,1,2)(0,0,1,2,0)(0,0,1,2,1)(0,0,1,2,2)(0,0,2,0,0)(0,0,2,0,1)(0,0,2,0,2)(0,0,2,1,0)(0,0,2,1,1)(0,0,2,1,2)(0,0,2,2,0)(0,0,2,2,1)(0,0,2,2,2)(0,1,0,0,0)(0,1,0,0,1)(0,1,0,0,2)(0,1,0,1,0)(0,1,0,1,1)(0,1,0,2,0)(0,1,0,2,2)(0,1,1,0,0)(0,1,1,0,1)(0,1,1,0,2)(0,1,1,1,0)(0,1,1,1,1)(0,1,1,2,0)(0,1,1,2,2)(0,1,2,0,0)(0,1,2,0,1)(0,1,2,0,2)(0,1,2,1,0)(0,1,2,1,2)(0,1,2,2,0)(0,1,2,2,1)(0,2,0,0,0)(0,2,0,0,1)(0,2,0,0,2)(0,2,0,1,0)(0,2,0,1,2)(0,2,0,2,0)(0,2,0,2,1)(0,2,1,0,0)(0,2,1,0,1)(0,2,1,0,2)(0,2,1,1,0)(0,2,1,1,2)(0,2,1,2,0)(0,2,1,2,1)(0,2,2,0,0)(0,2,2,0,1)(0,2,2,0,2)(0,2,2,1,0)(0,2,2,1,1)(0,2,2,2,0)(0,2,2,2,2)(1,0,0,0,0)(1,0,0,0,1)(1,0,0,0,2)(1,0,0,1,0)(1,0,0,1,2)(1,0,0,2,0)(1,0,0,2,1)(1,0,1,0,0)(1,0,1,0,1)(1,0,1,0,2)(1,0,1,1,0)(1,0,1,1,2)(1,0,1,2,0)(1,0,1,2,1)(1,0,2,0,0)(1,0,2,0,1)(1,0,2,0,2)(1,0,2,1,0)(1,0,2,1,1)(1,0,2,2,0)(1,0,2,2,2)(1,1,0,0,0)(1,1,0,0,1)(1,1,0,0,2)(1,1,0,1,0)(1,1,0,2,0)(1,1,1,0,0)(1,1,1,0,1)(1,1,1,0,2)(1,1,1,1,0)(1,1,1,2,0)(1,1,2,0,0)(1,1,2,0,1)(1,1,2,0,2)(1,1,2,1,0)(1,1,2,2,0)(1,2,0,0,0)(1,2,0,0,1)(1,2,0,0,2)(1,2,0,1,0)(1,2,0,2,0)(1,2,1,0,0)(1,2,1,0,1)(1,2,1,0,2)(1,2,1,1,0)(1,2,1,2,0)(1,2,2,0,0)(1,2,2,0,1)(1,2,2,0,2)(1,2,2,1,0)(1,2,2,2,0)(2,0,0,0,0)(2,0,0,0,1)(2,0,0,0,2)(2,0,0,1,0)(2,0,0,1,1)(2,0,0,2,0)(2,0,0,2,2)(2,0,1,0,0)(2,0,1,0,1)(2,0,1,0,2)(2,0,1,1,0)(2,0,1,1,1)(2,0,1,2,0)(2,0,1,2,2)(2,0,2,0,0)(2,0,2,0,1)(2,0,2,0,2)(2,0,2,1,0)(2,0,2,1,2)(2,0,2,2,0)(2,0,2,2,1)(2,1,0,0,0)(2,1,0,0,1)(2,1,0,0,2)(2,1,0,1,0)(2,1,0,2,0)(2,1,1,0,0)(2,1,1,0,1)(2,1,1,0,2)(2,1,1,1,0)(2,1,1,2,0)(2,1,2,0,0)(2,1,2,0,1)(2,1,2,0,2)(2,1,2,1,0)(2,1,2,2,0)(2,2,0,0,0)(2,2,0,0,1)(2,2,0,0,2)(2,2,0,1,0)(2,2,0,2,0)(2,2,1,0,0)(2,2,1,0,1)(2,2,1,0,2)(2,2,1,1,0)(2,2,1,2,0)(2,2,2,0,0)(2,2,2,0,1)(2,2,2,0,2)(2,2,2,1,0)(2,2,2,2,0)->S4 ; (1,0,0,1,1)(1,0,0,2,2)(1,0,1,1,1)(1,0,1,2,2)(1,0,2,1,2)(1,0,2,2,1)(1,1,0,1,1)(1,1,0,2,2)(1,1,1,1,1)(1,1,1,2,2)(1,1,2,1,2)(1,1,2,2,1)(1,2,0,1,2)(1,2,0,2,1)(1,2,1,1,2)(1,2,1,2,1)(1,2,2,1,1)(1,2,2,2,2)(2,0,0,1,2)(2,0,0,2,1)(2,0,1,1,2)(2,0,1,2,1)(2,0,2,1,1)(2,0,2,2,2)(2,1,0,1,2)(2,1,0,2,1)(2,1,1,1,2)(2,1,1,2,1)(2,1,2,1,1)(2,1,2,2,2)(2,2,0,1,1)(2,2,0,2,2)(2,2,1,1,1)(2,2,1,2,2)(2,2,2,1,2)(2,2,2,2,1)->S5 ; (0,1,0,1,2)(0,1,0,2,1)(0,1,1,1,2)(0,1,1,2,1)(0,1,2,1,1)(0,1,2,2,2)(0,2,0,1,1)(0,2,0,2,2)(0,2,1,1,1)(0,2,1,2,2)(0,2,2,1,2)(0,2,2,2,1)(1,1,0,1,2)(1,1,0,2,1)(1,1,1,1,2)(1,1,1,2,1)(1,1,2,1,1)(1,1,2,2,2)(1,2,0,1,1)(1,2,0,2,2)(1,2,1,1,1)(1,2,1,2,2)(1,2,2,1,2)(1,2,2,2,1)(2,1,0,1,1)(2,1,0,2,2)(2,1,1,1,1)(2,1,1,2,2)(2,1,2,1,2)(2,1,2,2,1)(2,2,0,1,2)(2,2,0,2,1)(2,2,1,1,2)(2,2,1,2,1)(2,2,2,1,1)(2,2,2,2,2)->S6
S2 (Consistant) : p ; p\/~p ; <<1,2,3,4,5>>XT
   Succ: (0,0,0,0,0)->S4
S3 (Consistant) : ~p ; p\/~p ; <<1,2,3,4,5>>XT
   Succ: (0,0,0,0,0)->S4
S4 (Consistant) : T ; <<1,2,3,4,5>>XT
   Succ: (0,0,0,0,0)->S4
S5 (Consistant) : ~c ; ~~~c ; <<1,2,3,4,5>>XT
   Succ: (0,0,0,0,0)->S4
S6 (Consistant) : c ; ~~c ; <<1,2,3,4,5>>XT
   Succ: (0,0,0,0,0)->S4

#2 Updated by Thorsten Wißmann over 3 years ago

  • Status changed from New to Closed

Also available in: Atom PDF