Mathematica 9 is now available
Services & Resources / Wolfram Forums / MathGroup Archive
-----

MathGroup Archive 2008

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

Search the Archive

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?







  • Prev by Date: Re: Path to *.m file
  • Next by Date: Re: NDSolve Question
  • Previous by thread: RE: A question regarding a hyperbolic geometric function
  • Next by thread: Re: Mathematica logic capabilities