Riener, M. (2011). Integrating theories into inference systems [Diploma Thesis, Technische Universität Wien]. reposiTUm. http://hdl.handle.net/20.500.12708/159961
Die Axiomatisierung arithmetischer Gesetze im Bereich des Automatischen Beweisens erzeugt viele für Menschen intuitive Ableitungsschritte. Bei der Analyse mathematischer Beweise mit der CERES Methode ist es von Vorteil, diese auszublenden. Diese Arbeit erweitert CERES um integrierte Gleichungstheorien. Dazu wird die Methode auf einen Sequenzenkalkül modulo und einen passenden Resolutionskalkül übertragen, welche beide dem Prinzip der Deduction Modulo entstammen. Als laufendes Beispiel wird die Theorie modulo kommutativer Monoide verwendet und mit der ursprünglichen Methode verglichen.<br />
de
The axiomatization of arithmetical properties in theorem proving creates many straightforward inference steps. In analyzing mathematical proofs with the CERES (Cut-Elimination by Resolution) system, it is convenient to hide these inferences. The central topic of the thesis is the extension of the CERES method to allow reasoning modulo equational theories. For this, the inference systems of Sequent Calculus modulo and Extended Narrowing and Resolution replace their non-equational counterparts in CERES. The method is illustrated by examples comparing inference modulo the theory of associativity and commutativity with unit element to inference in the empty theory.
