编程介的小学生 2017-04-26 05:01 采纳率: 20.5%
浏览 738
已采纳

Intuitionistic Logic

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 starts from an arbitrary acyclic oriented graph = (X, G). Then a partial order is constructed on X, the set of vertices of : for any x, y X we define x y iff there exists a path (possibly of zero length) in from x to y. Next, consider the set of all subsets of X and the set consisting of all X such that any two different x and y from are incomparable (i.e. neither x y nor y x). Note that always contains the empty set and all one-element subsets of X. Now it is possible to define a map Max : . For any M X we put Max(M) = { x M : y M : x y, x y} -- the set of all maximal elements of M .

Next we define several operations on . For any , put = Max(), = Max({ x X : y , z : x y, x z}), = {x : y : x y}, 0 = Max(X), 1 = , = (0), = (() ()).

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;
Conjuction -- E1 E2 ... En. Note that the conjunction is evaluated from left to right: E1E2E3 = (E1E2)E3.
Disjunction -- E1E2...En. The same remark applies.
Implication -- E1E2. Unlike the previous two operations it is evaluated from right to left: E1E2E3 means E1(E2E3).
Equivalence -- E1E2...En. This expression is equal to (E1E2)(E2E3)...(En-1En).
The operations are listed from the highest priority to the lowest.

A formula E will be called valid (in the model defined by ) if after substitution of arbitrary elements of for the variables involved in E it evaluates to 1; otherwise it is called invalid.

Your task is to determine for a given graph and a set of formulae which of them are valid and which invalid.

Input

Input consists of multiple test cases.
For each case the first line contains two integers N and M separated by a single space -- the number of vertices (1 N 100) and edges (0 M 5000) of . The next M lines contain two integers si and ti each -- the beginning and the end of 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 Hv[j] 106 where v[j] is the number of different variables used in j-th formula.
Output

For each test case, print K lines -- one line for each formula. Write to the j-th line either "valid" or "invalid".
There must be one blank line between two consecutive cases, but no extra line at the end.
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)
1 0
6
1=0
X|~X
A=>B=>C = (A&B)=>C
~~X => X
X => ~~X
(X => Y) = (Y | ~X)
Possible Output for Sample Input

invalid
invalid
valid
invalid
valid
invalid
valid
valid
invalid
valid
valid

invalid
valid
valid
valid
valid
valid

  • 写回答

1条回答 默认 最新

  • threenewbee 2017-05-10 15:52
    关注
    本回答被题主选为最佳回答 , 对您是否有帮助呢?
    评论

报告相同问题?

悬赏问题

  • ¥15 求差集那个函数有问题,有无佬可以解决
  • ¥15 【提问】基于Invest的水源涵养
  • ¥20 微信网友居然可以通过vx号找到我绑的手机号
  • ¥15 寻一个支付宝扫码远程授权登录的软件助手app
  • ¥15 解riccati方程组
  • ¥15 display:none;样式在嵌套结构中的已设置了display样式的元素上不起作用?
  • ¥15 使用rabbitMQ 消息队列作为url源进行多线程爬取时,总有几个url没有处理的问题。
  • ¥15 Ubuntu在安装序列比对软件STAR时出现报错如何解决
  • ¥50 树莓派安卓APK系统签名
  • ¥65 汇编语言除法溢出问题