15 found
Order:
  1. Epsilon theorems in intermediate logics.Matthias Baaz & Richard Zach - 2022 - Journal of Symbolic Logic 87 (2):682-720.
    Any intermediate propositional logic can be extended to a calculus with epsilon- and tau-operators and critical formulas. For classical logic, this results in Hilbert’s $\varepsilon $ -calculus. The first and second $\varepsilon $ -theorems for classical logic establish conservativity of the $\varepsilon $ -calculus over its classical base logic. It is well known that the second $\varepsilon $ -theorem fails for the intuitionistic $\varepsilon $ -calculus, as prenexation is impossible. The paper investigates the effect of adding critical $\varepsilon $ - (...)
    Download  
     
    Export citation  
     
    Bookmark   2 citations  
  2. Elimination of Cuts in First-order Finite-valued Logics.Matthias Baaz, Christian G. Fermüller & Richard Zach - 1993 - Journal of Information Processing and Cybernetics EIK 29 (6):333-355.
    A uniform construction for sequent calculi for finite-valued first-order logics with distribution quantifiers is exhibited. Completeness, cut-elimination and midsequent theorems are established. As an application, an analog of Herbrand’s theorem for the four-valued knowledge-representation logic of Belnap and Ginsberg is presented. It is indicated how this theorem can be used for reasoning about knowledge bases with incomplete and inconsistent information.
    Download  
     
    Export citation  
     
    Bookmark   18 citations  
  3. Systematic construction of natural deduction systems for many-valued logics.Matthias Baaz, Christian G. Fermüller & Richard Zach - 1993 - In Unknown (ed.), Proceedings of The Twenty-Third International Symposium on Multiple-Valued Logic, 1993. IEEE Press. pp. 208-213.
    A construction principle for natural deduction systems for arbitrary, finitely-many-valued first order logics is exhibited. These systems are systematically obtained from sequent calculi, which in turn can be automatically extracted from the truth tables of the logics under consideration. Soundness and cut-free completeness of these sequent calculi translate into soundness, completeness, and normal-form theorems for natural deduction systems.
    Download  
     
    Export citation  
     
    Bookmark   14 citations  
  4. Labeled calculi and finite-valued logics.Matthias Baaz, Christian G. Fermüller, Gernot Salzer & Richard Zach - 1998 - Studia Logica 61 (1):7-33.
    A general class of labeled sequent calculi is investigated, and necessary and sufficient conditions are given for when such a calculus is sound and complete for a finite -valued logic if the labels are interpreted as sets of truth values. Furthermore, it is shown that any finite -valued logic can be given an axiomatization by such a labeled calculus using arbitrary "systems of signs," i.e., of sets of truth values, as labels. The number of labels needed is logarithmic in the (...)
    Download  
     
    Export citation  
     
    Bookmark   19 citations  
  5. Dual Systems of Sequents and Tableaux for Many-Valued Logics.Matthias Baaz, Christian G. Fermüller & Richard Zach - 1993 - Bulletin of the EATCS 51:192-197.
    The aim of this paper is to emphasize the fact that for all finitely-many-valued logics there is a completely systematic relation between sequent calculi and tableau systems. More importantly, we show that for both of these systems there are al- ways two dual proof sytems (not just only two ways to interpret the calculi). This phenomenon may easily escape one’s attention since in the classical (two-valued) case the two systems coincide. (In two-valued logic the assignment of a truth value and (...)
    Download  
     
    Export citation  
     
    Bookmark   8 citations  
  6. Compact propositional Gödel logics.Matthias Baaz & Richard Zach - 1998 - In Baaz Matthias (ed.), 28th IEEE International Symposium on Multiple-Valued Logic, 1998. Proceedings. IEEE Press. pp. 108-113.
    Entailment in propositional Gödel logics can be defined in a natural way. While all infinite sets of truth values yield the same sets of tautologies, the entailment relations differ. It is shown that there is a rich structure of infinite-valued Gödel logics, only one of which is compact. It is also shown that the compact infinite-valued Gödel logic is the only one which interpolates, and the only one with an r.e. entailment relation.
    Download  
     
    Export citation  
     
    Bookmark   7 citations  
  7. Hypersequents and the proof theory of intuitionistic fuzzy logic.Matthias Baaz & Richard Zach - 2000 - In Clote Peter G. & Schwichtenberg Helmut (eds.), Computer Science Logic. 14th International Workshop, CSL 2000. Springer. pp. 187– 201.
    Takeuti and Titani have introduced and investigated a logic they called intuitionistic fuzzy logic. This logic is characterized as the first-order Gödel logic based on the truth value set [0,1]. The logic is known to be axiomatizable, but no deduction system amenable to proof-theoretic, and hence, computational treatment, has been known. Such a system is presented here, based on previous work on hypersequent calculi for propositional Gödel logics by Avron. It is shown that the system is sound and complete, and (...)
    Download  
     
    Export citation  
     
    Bookmark   6 citations  
  8. Quantified Propositional Gödel Logics.Matthias Baaz, Agata Ciabattoni & Richard Zach - 2000 - In Voronkov Andrei & Parigot Michel (eds.), Logic for Programming and Automated Reasoning. 7th International Conference, LPAR 2000. Springer. pp. 240-256.
    It is shown that Gqp↑, the quantified propositional Gödel logic based on the truth-value set V↑ = {1 - 1/n : n≥1}∪{1}, is decidable. This result is obtained by reduction to Büchi's theory S1S. An alternative proof based on elimination of quantifiers is also given, which yields both an axiomatization and a characterization of Gqp↑ as the intersection of all finite-valued quantified propositional Gödel logics.
    Download  
     
    Export citation  
     
    Bookmark   3 citations  
  9. 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.
    Download  
     
    Export citation  
     
    Bookmark   2 citations  
  10. Effective finite-valued approximations of general propositional logics.Matthias Baaz & Richard Zach - 2008 - In Arnon Avron & Nachum Dershowitz (eds.), Pillars of Computer Science: Essays Dedicated to Boris (Boaz) Trakhtenbrot on the Occasion of His 85th Birthday. Springer Verlag. pp. 107–129.
    Propositional logics in general, considered as a set of sentences, can be undecidable even if they have “nice” representations, e.g., are given by a calculus. Even decidable propositional logics can be computationally complex (e.g., already intuitionistic logic is PSPACE-complete). On the other hand, finite-valued logics are computationally relatively simple—at worst NP. Moreover, finite-valued semantics are simple, and general methods for theorem proving exist. This raises the question to what extent and under what circumstances propositional logics represented in various ways can (...)
    Download  
     
    Export citation  
     
    Bookmark  
  11. Completeness of a Hypersequent Calculus for Some First-order Gödel Logics with Delta.Matthias Baaz, Norbert Preining & Richard Zach - 2006 - In Baaz Matthias, Preining Norbert & Zach Richard (eds.), 36th Interna- tional Symposium on Multiple-valued Logic. May 2006, Singapore. Proceedings. IEEE Press.
    All first-order Gödel logics G_V with globalization operator based on truth value sets V C [0,1] where 0 and 1 lie in the perfect kernel of V are axiomatized by Ciabattoni’s hypersequent calculus HGIF.
    Download  
     
    Export citation  
     
    Bookmark  
  12. Algorithmic Structuring of Cut-free Proofs.Matthias Baaz & Richard Zach - 1993 - In Egon Börger, Gerhard Jäger, Hans Kleine Büning, Simone Martini & Michael M. Richter (eds.), Computer Science Logic. CSL’92, San Miniato, Italy. Selected Papers. Springer. pp. 29–42.
    The problem of algorithmic structuring of proofs in the sequent calculi LK and LKB ( LK where blocks of quantifiers can be introduced in one step) is investigated, where a distinction is made between linear proofs and proofs in tree form. In this framework, structuring coincides with the introduction of cuts into a proof. The algorithmic solvability of this problem can be reduced to the question of k-l-compressibility: "Given a proof of length k , and l ≤ k : Is (...)
    Download  
     
    Export citation  
     
    Bookmark  
  13. Short Proofs of Tautologies using the Schema of Equivalence.Matthias Baaz & Richard Zach - 1994 - In Egon Börger, Yuri Gurevich & Karl Meinke (eds.), Computer Science Logic. 7th Workshop, CSL '93, Swansea. Selected Papers. Springer. pp. 33-35.
    It is shown how the schema of equivalence can be used to obtain short proofs of tautologies A , where the depth of proofs is linear in the number of variables in A .
    Download  
     
    Export citation  
     
    Bookmark   1 citation  
  14. Incompleteness of a first-order Gödel logic and some temporal logics of programs.Matthias Baaz, Alexander Leitsch & Richard Zach - 1996 - In Kleine Büning Hans (ed.), Computer Science Logic. CSL 1995. Selected Papers. 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 (...)
    Download  
     
    Export citation  
     
    Bookmark   1 citation  
  15. Approximating Propositional Calculi by Finite-valued Logics.Matthias Baaz & Richard Zach - 1994 - In Baaz Matthias & Zach Richard (eds.), 24th International Symposium on Multiple-valued Logic, 1994. Proceedings. IEEE Press. pp. 257–263.
    The problem of approximating a propositional calculus is to find many-valued logics which are sound for the calculus (i.e., all theorems of the calculus are tautologies) with as few tautologies as possible. This has potential applications for representing (computationally complex) logics used in AI by (computationally easy) many-valued logics. It is investigated how far this method can be carried using (1) one or (2) an infinite sequence of many-valued logics. It is shown that the optimal candidate matrices for (1) can (...)
    Download  
     
    Export citation  
     
    Bookmark