Online Judge | Problem Set | Authors | Online Contests | User | ||||||
---|---|---|---|---|---|---|---|---|---|---|

Web Board Home Page F.A.Qs Statistical Charts | Current Contest Past Contests Scheduled Contests Award Contest |

Language: Intuitionistic Logic
Description Recently Vasya became acquainted with an interesting movement in mathematics and logic called “intuitionism”. The main idea of this movement consists in the rejection of the law of excluded middle (the logical law stating that any assertion is either true or false). Vasya liked this idea; he says: “Classical mathematics says that Fermat Last Theorem is either true or false; but this statement is completely useless for me until I see the proof or a contrary instance”. So Vasya became a born-again intuitionist. He tries to use the intuitionistic logic in all his activities and especially in his scientific work. But this logic is much more diffcult than the classic one. Vasya often tries to use logical formulae that are valid in classical logic but aren't so in the intuitionistic one. Now he wants to write a program that will help him to check the validity of his formulae automatically. He has found a book describing how to do that but unfortunately he isn’t good at programming, so you’ll have to help him. The construction start from an arbitrary acyclic oriented graph Next we define several operations on Now consider logical formulae consisting of the following symbols: - Constants 1 and 0;
- Variables – capital letters from A to Z;
- Parentheses – if
*E*is a formula, then (*E*) is another; - Negation – ¬
*E*is a formula for any formula*E*; - Conjunction –
*E*_{1}∧*E*_{2}∧ … ∧*E*. Note that the conjunction is evaluated from left to right:_{n}*E*_{1}∧*E*_{2}∧*E*_{3}= (*E*_{1}∧*E*_{2}) ∧*E*_{3}. - Disjunction –
*E*_{1}∨*E*_{2}∨ … ∨*E*. The same remark applies._{n} - Implication –
*E*_{1}⇒*E*_{2}. Unlike the previous two operations it is evaluated from right to left:*E*_{1}⇒*E*_{2}⇒*E*_{3}means*E*_{1}⇒ (*E*_{2}⇒*E*_{3}). - Equivalence –
*E*_{1}≡*E*_{2}≡ … ≡*E*. This expression is equal to (_{n}*E*_{1}≡*E*_{2}) ∧ (*E*_{2}≡*E*_{3}) ∧ … ∧ (*E*_{n − 1}≡*E*)._{n}
The operations are listed from the highest priority to the lowest. A formula Your task is to determine for a given graph Input For each case the first line contains two integers t each – the beginning and the end of _{i}i-th edge respectively. The next line contains K (1 ≤ K ≤ 20) – the number of formulae to be processed. The following K lines contain one formula each. A formula is represented as a string consisting of tokens 0, 1, A … Z, (, ), ~, &, |, =>, =. The last five tokens stand for ¬, ∧, ∨, ⇒ and ≡ respectively. Tokens can be separated by an arbitrary number of spaces. No line will be longer than 254 characters. All formulae in the file will be syntactically correct. Also you may assume that the number H = ||Η|| of elements of Η doesn’t exceed 100 and that the sum ∑_{1 ≤ j ≤ K} H^{v[j]} ≤ 10^{6} where v[j] is the number of different variables used in j-th formula.Output For each test case, print Sample Input 6 6 1 2 2 3 2 4 3 5 4 5 5 6 11 1=0 X|~X A=>B=>C = (A&B)=>C ~~X => X X => ~~X (X => Y) = (Y | ~X) A&(B|C) = A&B|A&C (X=>A)&(Y=>A) => X|Y=>A X = ~~X ~X=~~~X ~X = (X => 0) Sample Output invalid invalid valid invalid valid invalid valid valid invalid valid valid Source Northeastern Europe 2002, Northern Subregion |

[Submit] [Go Back] [Status] [Discuss]

All Rights Reserved 2003-2013 Ying Fuchen,Xu Pengcheng,Xie Di

Any problem, Please Contact Administrator