|
|
(forall x. exists y. J(x,y)) /\
(forall x. exists y. G(x,y)) /\
(forall x y. J(x,y) \/ G(x,y)
==> (forall z. J(y,z) \/ G(y,z) ==> H(x, z)))
==> (forall x. exists y. H(x,y))
-
Returns:
formula<fol>
|
|
|
(forall z.
exists w. forall x. exists y. (P(x,z) ==> P(y,w)) /\ P(y,z) /\
(P(y,w) ==> (exists u. Q(u,w)))) /\
(forall x z. ~P(x,z) ==> (exists y. Q(y,z))) /\
((exists x y. Q(x,y)) ==> (forall x. R(x,x))) ==>
(forall x. exists y. R(x,y))
-
Returns:
formula<fol>
|
|
|
(forall x.
P(a) /\ (P(x) ==> (exists y. P(y) /\ R(x,y))) ==>
(exists z w. P(z) /\ R(x,w) /\ R(w,z))) <=>
(forall x.
(~P(a) \/ P(x) \/ (exists z w. P(z) /\ R(x,w) /\ R(w,z))) /\
(~P(a) \/ ~(exists y. P(y) /\ R(x,y)) \/
(exists z w. P(z) /\ R(x,w) /\ R(w,z))))
-
Returns:
formula<fol>
|
|
|
~(exists x. forall y. P(y,x) <=> ~P(y,y))
-
Returns:
formula<fol>
|
|
|
(exists y. forall x. P(x,y) <=> P(x,x))
==> ~(forall x. exists y. forall z. P(z,y) <=> ~P(z,x))
-
Returns:
formula<fol>
|
|
|
(forall z. exists y. forall x. P(x,y) <=> P(x,z) /\ ~P(x,x))
==> ~(exists z. forall x. P(x,z))
-
Returns:
formula<fol>
|
|
|
~(exists y. forall x. P(x,y) <=> ~(exists z. P(x,z) /\ P(z,x)))
-
Returns:
formula<fol>
|
|
|
(forall x y. Q(x,y) <=> forall z. P(z,x) <=> P(z,y))
==> forall x y. Q(x,y) <=> Q(y,x)
-
Returns:
formula<fol>
|
|
|
(forall x. P(x) ==> (exists y. G(y) /\ H(x,y)) /\
(exists y. G(y) /\ ~H(x,y))) /\
(exists x. J(x) /\ (forall y. G(y) ==> H(x,y))) ==>
(exists x. J(x) /\ ~P(x))
-
Returns:
formula<fol>
|
|
|
(forall x.
P(x) /\ (forall y. G(y) /\ H(x,y) ==> J(x,y)) ==>
(forall y. G(y) /\ H(x,y) ==> R(y))) /\
~(exists y. L(y) /\ R(y)) /\
(exists x. P(x) /\ (forall y. H(x,y) ==>
L(y)) /\ (forall y. G(y) /\ H(x,y) ==> J(x,y))) ==>
(exists x. P(x) /\ ~(exists y. G(y) /\ H(x,y)))
-
Returns:
formula<fol>
|
|
|
(forall x. P(x) /\ (forall y. P(y) /\ H(y,x) ==> G(y)) ==> G(x)) /\
((exists x. P(x) /\ ~G(x)) ==>
(exists x. P(x) /\ ~G(x) /\
(forall y. P(y) /\ ~G(y) ==> J(x,y)))) /\
(forall x y. P(x) /\ P(y) /\ H(x,y) ==> ~J(y,x)) ==>
(forall x. P(x) ==> G(x))
-
Returns:
formula<fol>
|
|
|
lives(agatha) /\ lives(butler) /\ lives(charles) /\
(killed(agatha,agatha) \/ killed(butler,agatha) \/
killed(charles,agatha)) /\
(forall x y. killed(x,y) ==> hates(x,y) /\ ~richer(x,y)) /\
(forall x. hates(agatha,x) ==> ~hates(charles,x)) /\
(hates(agatha,agatha) /\ hates(agatha,charles)) /\
(forall x. lives(x) /\ ~richer(x,agatha) ==> hates(butler,x)) /\
(forall x. hates(agatha,x) ==> hates(butler,x)) /\
(forall x. ~hates(x,agatha) \/ ~hates(x,butler) \/ ~hates(x,charles))
==> killed(agatha,agatha) /\
~killed(butler,agatha) /\
~killed(charles,agatha)
-
Returns:
formula<fol>
|
