Services & ResourcesWolfram ForumsMathGroup Archive

[Date Index] [Thread Index] [Author Index]

Mathematica logic capabilities

• To: mathgroup at smc.vnet.net
• Subject: [mg86400] Mathematica logic capabilities
• From: magma <maderri2 at gmail.com>
• Date: Mon, 10 Mar 2008 02:05:30 -0500 (EST)

Mathematica is supposed to have an automated theorem prover.

I see that I can write an expression in propositional calculus and use
Reduce to determine whether it is a tautology (valid expression) or
not.
For example

Implies[Not[Not[p] \[And] Not[q]], p \[Or] q] // Reduce

gives True   (De Morgan law)

However it does not seem to be able to do the same with predicate
calculus.
For example:

Implies[ForAll[x, f[x]], Exists[x, f[x]]] // Reduce

returns an error, complaining that the expression is not quantized,
instead of returning true as it should.

So the question is: can Mathematica be used to do predicate calculus,
without extra packages?
If yes how?

• Follow-Ups:
  • Re: Mathematica logic capabilities
    • From: Andrzej Kozlowski <akoz@mimuw.edu.pl>