Prototype / Predicate Calculus
Based on the results of the propositional calculus here are predicate calculus theorems derived.
The following documents were generated again with the prototype out of qedeq modules. The qedeq modules were checked for formal correctness with the integrated proof verifier. (Also see last column.)
If the viewing of the HTML pages in the first column is not satisfactorily please try the second HTML links (o.html) which require an installed symbol font. If you have also trouble viewing these HTML pages please take look at Ian Hutchinson's pages: Browser Problems and Comparative Review of World-Wide-Web Mathematics Renderers.
Basic definitions of predicate logic
lang&rules |
|
html |
o.html |
|
|
|
|
informal definition of the used language and the rules of derivation |
predaxiom |
|
html |
o.html |
pdf |
tex |
qedeq |
|
additional axioms, and declarations of the rules of derivation of predicate calculus |
Simple derivations
With meta rules
The following variant of predtheo2 uses meta rules from rule version 1.02.00.
|