1,721,080 research outputs found
Cut-elimination in functional higher-order logic
Full text linkIt is known that there can be no elementary (reductive) proof of cut-elimination for a sequent calculus of higher-order logic, since this would provide an elementary proof of consistency of PA. Thus the cut-elimination proofs for higher-order calculi are either semantic (through Henkin semantics) or semi-semantic (through resolution, CERES). In this thesis I study a sub-logic of higher-order logic in which quantification is restricted to objects of functional type only. By functional type I mean all types of simple type theory without the occurrence of the Boolean type. Such restriction gives rise to a logic that has a manageable proof-theory and at the same time shares some interesting properties with full higher-order logic. First, I define syntax and semantics of two variants of such a logic and give the corresponding cut-elimination proofs. These are easy adaptations of the Gentzen's proof for LK: one just has to incorporate beta-eta-equality in the calculus and then repeat the argument for LK with equality. Thus, logic defined this way is proof-theoretically closer to LK than to the higher-order calculus. This becomes obvious by looking at a proof-preserving translation from functional higher-order proofs to first-order proofs that is defined in this thesis. In addition, such translation provides a new perspective on Skolemization and unification, which are both problematic in higher-order logic. Second, I study semantics of this logic: I show incompleteness wrt standard semantics and give a completeness proof wrt general semantics based on Schuütte's reduction tree method. This is a simpler and more elegant way of proving this result than a more obvious specialization of a Henkin-style completeness proof for full higher-order logic
Cut elimination in inductive proofs of weakly quantified theorems
Full text linkIn dieser Arbeit wird erst der Gentzensche Beweis der Konsistenz der Peano- arithmetik vorgestellt, dann wird die Methode auf eine Klasse induktiver Be- weise erweitert. Da die Schnittregel in der Peanoarithmetik nicht redundant ist, ist Schnittelimination nur für Teilklassen möglich; hier wird die Teilklasse aller induktiven Beweise von Sätzen ohne starke Quantoren untersucht. Es wird gezeigt, dass bei dieser Klasse alle essentiellen Schnitte eliminiert werden können.After presenting Gentzen's cut elimination theorem and the proof of the consistency of Peano arithmetic, we extend the cut elimination procedure to a certain class of inductive proofs. Cut elimination is possible only on subclasses of all inductive proofs. We will investigate the subclass of inductive proofs of theorems without strong quantifiers.We will show that all inductions can be removed following Gentzen's proof of the consistency of Peano arithmetic and therefore, that essential cuts are redundant
Going Beyond Counting First Authors in Author Co-citation Analysis
Full text linkThe present study examines one of the fundamental aspects of author co-citation analysis (ACA) - the way co-citation
counts are defined. Co-citation counting provides the data on which all subsequent statistical analyses and mappings
are based, and we compare ACA results based on two different types of co-citation counting - the traditional type that
only counts the first one among a cited work's authors on the one hand and a non-traditional type that takes into
account the first 5 authors of a cited work on the other hand. Results indicate that the picture produced through this non-traditional author co-citation counting contains more coherent author groups and is therefore considerably clearer. However, this picture represents fewer specialties in the research field being studied than that produced through the traditional first-author co-citation counting when the same number of top-ranked authors is selected and analyzed. Reasons for these effects are discussed
CERES and fast cut-elimination
No full textEs ist bekannt dass die Komplexitat der Schnittelimination im allgemeinen Fall nonelementar ist. In dieser Arbeit werden Klassen von Beweisen charakterisiert welche eine schnelle (elementare) Schnittelimination zulassen. Zuerst werden der Sequentialkalkul und der Resolutionskalkul eingefuhrt. Anschliessend werden zwei Methoden der Schnittelimination, die Methode von Gentzen und CERES (cut-elimination by resolution), beschrieben. Es wird gezeigt, dass CERES die Gentzen Methode nonelementar beschleunigt. Die Methode CERES wird dann verwendet um schnelle Schnitteliminationsklassen zu definieren. Einige der bekannten Klassen werden erweitert und nachgewiesen, dass die Schnittelimination schnell bleibt. Schliesslich wird eine neue Klasse ONEQ eingefuhrt und (ebenfalls mit der CERES-Methode) nachgewiesen, dass schnelle Schnittelimination auf ONEQ moglich ist
Models of hypercomputation
Full text linkDer Darlegung von Grundsätzen der Berechenbarkeitstheorie folgt die Diskussion einiger Versionen und Interpretationen der sogenannten Church-Turing- These. Anschließend wird eine formale Definition der Hyperberechenbarkeit gegeben. Daraufhin werden einige abstrakte und physikalische Hypermaschinenmodelle aus der Literatur präsentiert. Diese sind in erster Linie Turingmaschinen mit unendlicher Zeit, Quantencomputer und relativistische Maschinenmodelle.Grundlegende Prinzipien dieser Modelle und ihre Rechenkraft werden diskutiert.After presenting preliminary knowledge in Computability Theory, some versions and interpretations of the so called Church-Turing thesis will be discussed.A formal definition of hypercomputation will be given. Some proposed abstract and physical hypermachine models from the literature will be presented. These will be (mainly) innite time Turing machines, quantum computers and relativistic machine models. Basic principles behind these models and their computational power will be discussed
Herbrand sequents and the Skolem-free CERES method
Full text linkA branch of mathematical logic is proof theory, which considers proofs as formal objects and is concerned with the analysis of their properties. One of the main theorems in proof theory is the cut-elimination theorem. It was proved by Gerhard Gentzen and states that the so-called cut-rule can always be eliminated from a formal proof system in the style of the sequent calculus LK. In real mathematical proofs, cut-elimination can be regarded as a method for eliminating lemmas. One property of cut-free proofs is that they only use subformulas of the formulas that are already present in the statement which has to be proved, i.e. they have the subformula-property. Gentzen's cut-elimination method is regarded as reductive cut-elimination. This method does not analyse the whole proof, but performs local proof rewriting steps on small parts of the proof. Another approach to cut-elimination is the method CERES (cut-elimination by resolution). In this method all cuts are analysed simultaneously and hence the global structure of the proof is taken into account. Roughly speaking, CERES extracts an unsatisfiable set of clauses, that encodes the structure of a proof containing cuts. A resolution refutation of this set of clauses serves as a skeleton for a proof containing at most atomic cuts. CERES-omegawas developed as CERES-method for higher-order logic and works, in contrast to CERES, with Skolem-free end-sequents. For the cut-elimination a new sequent calculus, LKsk, is introduced which does not contain the cut-rule. In the course of this work the idea of Skolem-free proofs was transferred to first-order logic, to gain a CERES-method which works in the presence of strong quantifiers in the end-sequent. We concentrate on the extraction of Herbrand sequents instead of the construction of the ACNF, a proof with at most atomic cuts. In the original CERES-method Herbrand sequents were extracted from the ACNF. We show, that the ACNF is not needed for the extraction and that the Herbrand sequents can be extracted from the resolution refutation and the corresponding projections. Our method for the extraction of Herbrand sequents is exponentially faster than the original, Skolem-free method.Ein Teilgebiet der mathematischen Logik ist die Beweistheorie, welche Beweise als formale Objekte betrachtet und deren Eigenschaften untersucht. Einer der wichtigsten Sätze der Beweistheorie ist der Satz der Schnittelimination. Dieser wurde von Gerhard Gentzen bewiesen und besagt, dass die sogenannte Schnittregel aus einem formalen Beweissystem (in der Art des Sequentialkalküls LK) immer enfernt werden kann. Die Schnittelimination kann in konkreten mathematischen Beweisen als eine Methode zum Entfernen von Hilfssätzen (Lemmata) angesehen werden. Eine Eigenschaft schnittfreier Beweise ist, dass sie nur Teilformeln der Formeln im zu beweisenden Satz enthalten, d.h. dass sie die Teilformel-Eigenschaft besitzen. Gentzen-s Methode zur Schnittelimination wird als reduktive Schnittelimination betrachtet. Hier betrachtet man nicht den gesamten Beweis, sondern führt lokale Beweistransformationen an einem Teil des gesamten Beweises durch. CERES (cut-elimination by resolution) stellt einen alternativen Ansatz dar. Hier werden alle Schnitte gleichzeitig analysiert und somit wird die globale Struktur des Beweises berücksichtigt. Grob gesagt wird eine widerlegbare Klauselmenge extrahiert, welche die Struktur eines Beweises mit Schnitten repräsentiert. Die Resolutionswiderlegung dieser Klauselmenge dient als Skelett für einen Beweis, der höchstens atomare Schnitte enthält. CERES! wurde als CERES-Methode für Logik höherer Ordnung entwickelt und arbeitet, im Gegensatz zu CERES, mit skolemfreien End-Sequenten. Für die Schnittelimination wird ein neuer Sequentialkalkül, LKsk, eingeführt, der keine Schnittregel enthält. Im Zuge dieser Arbeit wurde die Idee von skolemfreien Beweisen auf Logik erster Ordnung überführt, um eine CERES-Methode zu entwickeln, welche auch mit starken Quantoren im End-Sequent arbeiten kann. Wir konzentrieren uns auf die Extraktion von Herbrand Sequenten und nicht auf das Erzeugen der ACNF, welche ein Beweis mit höchstens atomaren Schnitten ist. Herbrand Sequente wurden in der ursprünglichen CERES-Methode aus der ACNF erzeugt. Wir zeigen, dass man für die Extraktion die ACNF nicht benötigt und dass man die Herbrand Sequente bereits aus der Resolutionswiderlegung und den zugehörigen Projektionen gewinnen kann. Unsere Methode zur Extraktion von Herbrand Sequenten ist exponentiell schneller als die ursprüngliche skolemfreie Methode
Integrating theories into inference systems
No full textDie 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.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
Anwendungen der Schnittelimination höherer Stufe
Full text linkThe method of Cut-Elimination by Resolution (CERES) bridges the fields of proof theory and automated theorem proving. Its proof theoretic value lies in the extraction of information from a theorem beyond its mere truth while its contribution to the automated theorem proving community lies in the generation of hard problems for which, at least in theory, a proof can always be found. An example for such a successful analysis in first-order logic was the formalization of Fürstenberg’s proof of the infinity of primes. So far, CERES!, the extension of CERES to higher-order logic was missing an application of equivalent complexity. This thesis develops the CERES! method further, improving the interplay with automated higher-order theorem provers. Furthermore we explore the use of expansion proofs as a concise representation of witness terms for weak quantifiers, the essential information generated by CERES. Moreover, we introduce CERES! =, a variant which targets the fragment of functional quantification with first-order equality and definition rules. Finally, we introduce LLK, a LATEX inspired proof input language and Sunburst trees, a global visualization of sequent calculus proofs and the implementation of these proof analysis techniques in the GAPT system. As a case study, we formalize the infinite pigeon hole principle and extract functions enumerating arbitrary many pigeons in the infinite-sized hole. We compare our results to those of Ratiu and Trifonov which were found via A-translation and modified Realizability. Simultaneously, we explore the gradient of solvable problems for higher-order provers, identifying possible directions for future development
- …
