11 found
Order:
  1.  16
    Cut Normal Forms and Proof Complexity.Matthias Baaz & Alexander Leitsch - 1999 - Annals of Pure and Applied Logic 97 (1-3):127-177.
    Statman and Orevkov independently proved that cut-elimination is of nonelementary complexity. Although their worst-case sequences are mathematically different the syntax of the corresponding cut formulas is of striking similarity. This leads to the main question of this paper: to what extent is it possible to restrict the syntax of formulas and — at the same time—keep their power as cut formulas in a proof? We give a detailed analysis of this problem for negation normal form , prenex normal form and (...)
    Direct download (4 more)  
     
    Export citation  
     
    Bookmark   7 citations  
  2. Completeness of a First-Order Temporal Logic with Time-Gaps.Matthias Baaz, Alexander Leitsch & Richard Zach - 1996 - Theoretical Computer Science 160 (1-2):241-270.
    The first-order temporal logics with □ and ○ of time structures isomorphic to ω (discrete linear time) and trees of ω-segments (linear time with branching gaps) and some of its fragments are compared: the first is not recursively axiomatizable. For the second, a cut-free complete sequent calculus is given, and from this, a resolution system is derived by the method of Maslov.
    Direct download (3 more)  
     
    Export citation  
     
    Bookmark   2 citations  
  3. Incompleteness of a First-Order Gödel Logic and Some Temporal Logics of Programs.Matthias Baaz, Alexander Leitsch & Richard Zach - 1996 - In Hans Kleine Büning (ed.), Computer Science Logic. CSL 1995. Selected Papers. Berlin: Springer. pp. 1--15.
    It is shown that the infinite-valued first-order Gödel logic G° based on the set of truth values {1/k: k ε w {0}} U {0} is not r.e. The logic G° is the same as that obtained from the Kripke semantics for first-order intuitionistic logic with constant domains and where the order structure of the model is linear. From this, the unaxiomatizability of Kröger's temporal logic of programs (even of the fragment without the nexttime operator O) and of the authors' temporal (...)
    Direct download (3 more)  
     
    Export citation  
     
    Bookmark  
  4.  77
    CERES in Higher-Order Logic.Stefan Hetzl, Alexander Leitsch & Daniel Weller - 2011 - Annals of Pure and Applied Logic 162 (12):1001-1034.
    We define a generalization of the first-order cut-elimination method CERES to higher-order logic. At the core of lies the computation of an set of sequents from a proof π of a sequent S. A refutation of in a higher-order resolution calculus can be used to transform cut-free parts of π into a cut-free proof of S. An example illustrates the method and shows that can produce meaningful cut-free proofs in mathematics that traditional cut-elimination methods cannot reach.
    Direct download (4 more)  
     
    Export citation  
     
    Bookmark   1 citation  
  5.  19
    On Different Concepts of Resolution.Alexander Leitsch - 1989 - Zeitschrift fur mathematische Logik und Grundlagen der Mathematik 35 (1):71-77.
    No categories
    Direct download  
     
    Export citation  
     
    Bookmark   2 citations  
  6.  15
    Complexity of Resolution Proofs and Function Introduction.Matthias Baaz & Alexander Leitsch - 1992 - Annals of Pure and Applied Logic 57 (3):181-215.
    The length of resolution proofs is investigated, relative to the model-theoretic measure of Herband complexity. A concept of resolution deduction is introduced which is somewhat more general than the classical concepts. It is shown that proof complexity is exponential in terms of Herband complexity and that this bound is tight. The concept of R-deduction is extended to FR-deduction, where, besides resolution, a function introduction rule is allowed. As an example, consider the clause P Q: conclude P) Q, where a, f (...)
    Direct download (4 more)  
     
    Export citation  
     
    Bookmark   2 citations  
  7. Computational Logic and Proof Theory 5th Kurt Gödel Colloquium, Kgc '97, Vienna, Austria, August 25-29, 1997 : Proceedings'. [REVIEW]G. Gottlob, Alexander Leitsch, Daniele Mundici & Kurt Gödel Society - 1997
     
    Export citation  
     
    Bookmark  
  8.  7
    On Different Concepts of Resolution.Alexander Leitsch - 1989 - Mathematical Logic Quarterly 35 (1):71-77.
    Direct download  
     
    Export citation  
     
    Bookmark   2 citations  
  9. Alexander Leitsch/From the Editor 3–5 Matthias Baaz and Rosalie Iemhoff/Gentzen Calculi for the Existence Predicate 7–23 Ulrich Berger, Stefan Berghofer, Pierre Letouzey and Helmut Schwichtenberg/Program Extraction From. [REVIEW]Alexander Leitsch - 2006 - Studia Logica 82:40.
     
    Export citation  
     
    Bookmark  
  10.  15
    Ceres in Intuitionistic Logic.David Cerna, Alexander Leitsch, Giselle Reis & Simon Wolfsteiner - 2017 - Annals of Pure and Applied Logic 168 (10):1783-1836.
    Direct download (3 more)  
     
    Export citation  
     
    Bookmark  
  11.  15
    2001 European Summer Meeting of the Association for Symbolic Logic Logic Colloquium'01.Itay Neeman, Alexander Leitsch, Toshiyasu Arai, Steve Awodey, James Cummings, Rod Downey & Harvey Friedman - 2002 - Bulletin of Symbolic Logic 8 (1):111-180.