((turnip ?x) -> (bitter ?x))
-> implication,
~ negation, V disjunction (or),
& conjunction (and),
A universal quantification (forall),
E existential quantification (exists)
?
~ V & -> ) group
propositions into expressions
whose truth values are defined (in truth tables)
as a function of the truth values of
the propositions which are connected
- (p -> q) <=> (~p V q)
- (~ (~ p)) <=> p
- (~ (p & q)) <=> ((~ p) V (~ q))
- (~ (p V q)) <=> ((~ p) & (~ q))
- (p V (q & r)) <=> ((p V q) & (p V r))
- (p & (q V r)) <=> ((p & q) V (p & r))
- (~ (A (?x) (p ?x))) <=> (E (?x) (~ (p ?x)))
- (~ (E (?x) (p ?x))) <=> (A (?x) (~ (p ?x)))
(E (?x) (p ?x)) --------------- (p x003) (A (?x) (E (?y) (p ?x ?y))) --------------------------- (A (?x) (p ?x (f004 ?x)))where
x003 and f004
are new object and function constants.
Last updated: 6 February 1996
URL: http://www.indiana.edu/~gasser/Q351/pred_calc.html
Comments:
gasser@salsa.indiana.edu
Copyright 1996,
The Trustees of
Indiana University