www.qedeq.org

 Hilbert II

English   Deutsch
Hilbert II at SourceForge
introduction
news
mathematics
QEDEQ
planning
download
glossary
development
prototype
installation
manual
propositional calculus
predicate calculus
QEDEQ
problems
links
contact
site map
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

predtheo1   html o.html pdf tex qedeq   first theorem
predtheo2   html o.html pdf tex qedeq   further theorems

With meta rules

The following variant of predtheo2 uses meta rules from rule version 1.02.00.

predtheo2'   html o.html pdf tex qedeq   further theorems

update 2014-01-20 09:20:48+0100