Syntax

The input must be a formula of pure first-order logic. Do not use free variables, names, identity or mathematical functions. Expressions containing these symbols are accepted as well-formed but do not evaluate properly.

This is the key for Input Forms of Traditional Forms:

Traditional Form	Input Form	Alternative Input Form
∀var scope	ForAll[var, scope]	A[var, scope]
∃var scope	Exists[var, scope]	E[var, scope]
¬ p	Not[p]	!p, !(p)
p ⋀ q	And[p,q]	p && q, (p && q)
p ⋁ q	Or[p,q]	p || q, (p || q)
p → q	Implies[p,q]
p ≡ q	Equivalent[p,q]
p ⊽ q	Nor[p,q]
p ⊼ q	Nand[p,q]
p ⊻ q	Xor[p,q]

The most convenient way is to use the alternative Input Form; do not use Traditional Form. If you use "!" instead of "Not", then use "!p" or "!(p)" but not "![p]". Be aware to use exactly 2 arguments in case of Implies and at least two arguments in case of And, Or, Equivalent, Nor, Nand and Xor. If you use only one argument, the respective formula is not well-formed but accepted by Mathematica. Be aware to use brackets of form "[" and "]" to signify the scope of quantifiers. Use "(" and ")" only in case of "!", "&&" and "||".

The following examples may help to get used to the syntax in the Mathematica style:

Traditional Form	Input Form
$p\wedge {\exists }_y{\exists }_z\neg f\left(z,y\right)\wedge {\forall }_{x}f\left(x,x\right)$	p && E[y, E[z, !f[z,y]]] && A[x, f[x,x]]
${\forall }_x{\exists }_{y}A\left(z,f\left(x,y\right)\wedge \neg f\left(z,z\right)\right)$	A[x, E[y, A[z, f[x,y] && !f[z,z]]]]
$\neg \left({\exists }_y{\forall }_{x}f\left(x,y\right)\wedge {\forall }_x{\exists }_{y}f\left(x,y\right)\right)$	Not[A[x, E[y, f[x,y]]] && E[y, A[x, f[x,y]]]]
${\forall }_x{\exists }_y\left(f\left(x,y\right)\wedge f\left(y,y\right)\wedge \neg f\left(x,x\right)\wedge \neg f\left(y,x\right)\right)$	A[x, E[y, f[x,y] && !f[y,x] && f[y,y] && !f[x,x]]]
${\forall }_x{\exists }_y{\forall }_z\left(f\left(x,y\right)\wedge \neg f\left(x,x\right)\wedge \left(f\left(x,z\right)\vee \neg f\left(y,z\right)\right)\right)$	A[x, E[y, A[z, f[x,y] && !f[x,x] && (!f[y,z] || f[x,z])]]]
${\forall }_{x\left(1\right)}{\exists }_{y\left(1\right)}{\exists }_{y\left(2\right)}{\forall }_{x\left(2\right)}\left(f\left(x\left(1\right),y\left(1\right)\right)\wedge \neg f\left(y\left(2\right),x\left(2\right)\right)\right)$	A[x[1], E[y[1], E[y[2],A[x[2],f[x[1],y[1]] && !f[y[2],x[2]]]]]]

Further examples:

Traditional Form:	${\forall }_{x\left(1\right)}{\exists }_{x\left(2\right)}{\exists }_{x\left(3\right)}{\forall }_{x\left(4\right)}{\exists }_{x\left(5\right)}\left(f\left(x\left(2\right),x\left(1\right),x\left(5\right)\right)\wedge \neg f\left(x\left(4\right),x\left(3\right),x\left(5\right)\right)\right)$
Input Form:	A[x[1], E[x[2], E[x[3], A[x[4], E[x[5], f[x[2], x[1], x[5]] && ! f[x[4], x[3], x[5]]]]]]]
Traditional Form:	${\forall }_{x\left(1\right)}{\exists }_{y\left(1\right)}{\forall }_{x\left(2\right)}{\exists }_{y\left(2\right)}\left(\left(f\left(x\left(1\right),y\left(1\right)\right)\wedge \neg f\left(y\left(2\right),x\left(2\right)\right)\right)\vee \left(f\left(x\left(1\right),x\left(2\right)\right)\wedge \neg f\left(y\left(1\right),y\left(2\right)\right)\right)\right)$
Input Form:	A[x[1], E[y[1], A[x[2], E[y[2], ((f[x[1], y[1]] && !f[y[2], x[2]]) || (!f[y[1], y[2]] && f[x[1], x[2]]))]]]]
Traditional Form:	${\forall }_{x\left(1\right)}{\exists }_{y\left(1\right)}{\exists }_{y\left(2\right)}{\forall }_{x\left(2\right)}{\exists }_{y\left(3\right)}\left(f\left(y\left(1\right),x\left(1\right),y\left(3\right)\right)\wedge f\left(y\left(1\right),x\left(2\right),y\left(3\right)\right)\wedge \neg f\left(x\left(2\right),y\left(2\right),y\left(3\right)\right)\right)$
Input Form:	A[x[1], E[y[1], E[y[2], A[x[2], E[y[3], (f[y[1],x[1],y[3]] && f[y[1],x[2],y[3]] && ! f[x[2],y[2],y[3]])]]]]]
Traditional Form:	${\forall }_{y\left(1\right)}{\exists }_x{\forall }_{y\left(2\right)}\left(\neg Q\left(y\left(1\right),y\left(1\right)\right)\wedge \left(\neg P\left(y\left(1\right),y\left(2\right)\right)\vee Q\left(x,y\left(2\right)\right)\right)\wedge \left(\neg Q\left(y\left(1\right),y\left(2\right)\right)\vee Q\left(x,y\left(2\right)\right)\right)\wedge P\left(y\left(1\right),y\left(1\right)\right)\right)$
Input Form:	A[y[1],E[x,A[y[2],P[y[1], y[1]] && (!P[y[1], y[2]] || Q[x, y[2]]) && (!Q[y[1], y[2]] || Q[x, y[2]]) && !Q[y[1], y[1]]]]]
Traditional Form:	${\exists }_{y\left(1\right)}\left({\exists }_{y\left(2\right)}\left({\exists }_{y\left(3\right)}\left(g\left(y\left(1\right),y\left(3\right)\right)\wedge g\left(y\left(3\right),y\left(2\right)\right)\right)\wedge \neg f\left(y\left(2\right)\right)\right)\wedge f\left(y\left(1\right)\right)\right)\wedge {\forall }_{x\left(1\right)}\left({\forall }_{x\left(2\right)}\left(f\left(x\left(2\right)\right)\vee \neg g\left(x\left(1\right),x\left(2\right)\right)\right)\vee \neg f\left(x\left(1\right)\right)\right)$
Input Form:	A[x[1], !f[x[1]] || A[x[2], f[x[2]] || !g[x[1],x[2]]]] && E[y[1], f[y[1]] && E[y[2], !f[y[2]] && E[y[3], g[y[1], y[3]] && g[y[3], y[2]]]]]
Traditional Form:	${\exists }_{y\left(1\right)}{\exists }_{y\left(2\right)}{\forall }_{x\left(1\right)}\left({\exists }_{y\left(3\right)}\left(f\left(x\left(1\right),y\left(3\right)\right)\wedge {\forall }_{x\left(2\right)}h\left(x\left(2\right),y\left(3\right)\right)\wedge \neg f\left(y\left(1\right),y\left(3\right)\right)\right)\vee {\exists }_{y\left(4\right)}\left({\forall }_{x\left(3\right)}\neg h\left(y\left(4\right),x\left(3\right)\right)\wedge g\left(x\left(1\right),y\left(4\right)\right)\wedge \neg g\left(y\left(2\right),y\left(4\right)\right)\right)\right)$
Input Form:	E[y[1], E[y[2], A[x[1], (E[y[3], f[x[1],y[3]] && !f[y[1], y[3]] && A[x[2], h[x[2], y[3]]]]) || (E[y[4], g[x[1], y[4]] && ! g[y[2], y[4]] && A[x[3], ! h[y[4], x[3]]]])]]]
Traditional Form:	${\exists }_{y\left(6\right)}\left({\exists }_{y\left(3\right)}\left(f\left(y\left(3\right),y\left(6\right)\right)\wedge {\forall }_{x\left(1\right)}\left({\exists }_{y\left(2\right)}\left({\exists }_{y\left(1\right)}f\left(y\left(2\right),y\left(1\right)\right)\wedge f\left(y\left(2\right),x\left(1\right)\right)\right)\vee f\left(y\left(3\right),x\left(1\right)\right)\right)\right)\wedge {\forall }_{x\left(2\right)}\left({\exists }_{y\left(5\right)}\left({\exists }_{y\left(4\right)}f\left(y\left(5\right),y\left(4\right)\right)\wedge f\left(y\left(5\right),x\left(2\right)\right)\right)\vee f\left(y\left(6\right),x\left(2\right)\right)\right)\right)$
Input Form:	E[y[6],E[y[3],f[y[3],y[6]] && A[x[1],E[y[2], E[y[1], f[y[2], y[1]]] && f[y[2], x[1]]] || f[y[3], x[1]]]] && A[x[2], E[y[5], E[y[4], f[y[5], y[4]]] && f[y[5], x[2]]] || f[y[6], x[2]]]]

Datenschutzerklaerung

© Timm Lampert / 2018-04-09