Prototyp / Prädikatenlogik
Aufbauend aus den Ergebnissen der Aussagenlogik werden hier nun prädikatenlogische Sätze hergeleitet.
Die folgenden Seiten wurden wiederum mit dem Prototypen aus Qedeq-Modulen generiert und zuvor von einem Beweisprüfer auf formale Korrektheit hin kontrolliert. (Siehe auch die letzte Spalte.)
Falls das Betrachten der in der ersten Spalte referenzierten HTML-Seiten Probleme bereitet, versuchen Sie bitte die zweiten HTML-Links (o.html), die auf Seiten verweisen, welche einen installierten Symbol-Font voraussetzen. Falls auch diese HTML-Seiten nicht richtig dargestellt werden, schauen Sie bitte auf Ian Hutchinson's Seiten nach: Browser Problems und Comparative Review of World-Wide-Web Mathematics Renderers.
Grundlegende Definitionen der Prädikatenlogik
lang&rules |
|
html |
o.html |
|
|
|
|
informelle Definition der verwendeten Sprache und der Schlussregeln |
predaxiom |
|
html |
o.html |
pdf |
tex |
qedeq |
|
zusätzliche Axiome und Deklarationen der Schlussregeln der Prädikatenlogik |
Einfache Herleitungen
Mit Metaregeln
Die folgende Variante von predtheo2 benutzt die Metaregeln der Regelversion 1.02.00.
|