18 found
Order:
Disambiguations
Martin Bunder [16]Martin W. Bunder [2]
  1.  14
    Completeness of Two Systems of Illative Combinatory Logic for First-Order Propositional and Predicate Calculus.Wil Dekkers, Martin Bunder & Henk Barendregt - 1998 - Archive for Mathematical Logic 37 (5-6):327-341.
    Illative combinatory logic consists of the theory of combinators or lambda calculus extended by extra constants (and corresponding axioms and rules) intended to capture inference. The paper considers 4 systems of illative combinatory logic that are sound for first-order propositional and predicate calculus. The interpretation from ordinary logic into the illative systems can be done in two ways: following the propositions-as-types paradigm, in which derivations become combinators, or in a more direct way, in which derivations are not translated. Both translations (...)
    Direct download (4 more)  
     
    Export citation  
     
    My bibliography   1 citation  
  2.  27
    Systems of Illative Combinatory Logic Complete for First-Order Propositional and Predicate Calculus.Henk Barendregt, Martin Bunder & Wil Dekkers - 1993 - Journal of Symbolic Logic 58 (3):769-788.
    Illative combinatory logic consists of the theory of combinators or lambda calculus extended by extra constants (and corresponding axioms and rules) intended to capture inference. The paper considers systems of illative combinatory logic that are sound for first-order propositional and predicate calculus. The interpretation from ordinary logic into the illative systems can be done in two ways: following the propositions-as-types paradigm, in which derivations become combinators or, in a more direct way, in which derivations are not translated. Both translations are (...)
    Direct download (8 more)  
     
    Export citation  
     
    My bibliography   1 citation  
  3.  21
    Completeness of the Propositions-as-Types Interpretation of Intuitionistic Logic Into Illative Combinatory Logic.Wil Dekkers, Martin Bunder & Henk Barendregt - 1998 - Journal of Symbolic Logic 63 (3):869-890.
    Illative combinatory logic consists of the theory of combinators or lambda calculus extended by extra constants (and corresponding axioms and rules) intended to capture inference. In a preceding paper, [2], we considered 4 systems of illative combinatory logic that are sound for first order intuitionistic propositional and predicate logic. The interpretation from ordinary logic into the illative systems can be done in two ways: following the propositions-as-types paradigm, in which derivations become combinators, or in a more direct way, in which (...)
    Direct download (8 more)  
     
    Export citation  
     
    My bibliography  
  4.  11
    1993 Annual Meeting of the Australasian Association for Logic, Adelaide, Australia, July 9-11, 1993.Martin Bunder - 1994 - Journal of Symbolic Logic 59 (4):1443-1449.
  5.  15
    On Adding (Ξ) to Weak Equality in Combinatory Logic.Martin W. Bunder, J. Roger Hindley & Jonathan P. Seldin - 1989 - Journal of Symbolic Logic 54 (2):590-607.
    Because the main difference between combinatory weak equality and λβ-equality is that the rule \begin{equation*}\tag{\xi} X = Y \vdash \lambda x.X = \lambda x.Y\end{equation*} is valid for the latter but not the former, it is easy to assume that another way of defining combinatory β-equality is to add rule (ξ) to the postulates for weak equality. However, to make this true, one must choose the definition of combinatory abstraction in (ξ) very carefully. If one tries to use one of the (...)
    Direct download (7 more)  
     
    Export citation  
     
    My bibliography  
  6.  8
    Pure Type Systems with More Liberal Rules.Martin Bunder & Wil Dekkers - 2001 - Journal of Symbolic Logic 66 (4):1561-1580.
    Pure Type Systems, PTSs, introduced as a generalisation of the type systems of Barendregt's lambda-cube, provide a foundation for actual proof assistants, aiming at the mechanic verification of formal proofs. In this paper we consider simplifications of some of the rules of PTSs. This is of independent interest for PTSs as this produces more flexible PTS-like systems, but it will also help, in a later paper, to bridge the gap between PTSs and systems of Illative Combinatory Logic. First we consider (...)
    Direct download (7 more)  
     
    Export citation  
     
    My bibliography  
  7.  1
    E-Mail:.][・, ヲ, ィ ァ ゥ・ ヲ ヲ・ ヲ ヲ・[!"# ァ $" &%'ァ (!%.Martin Bunder - 2004 - Bulletin of Symbolic Logic 10 (3).
    Direct download  
     
    Export citation  
     
    My bibliography  
  8.  1
    Intersection Types for Lambda-Terms and Combinators and Their Logics.Martin Bunder - 2002 - Logic Journal of the IGPL 10 (4):357-378.
    It is well known that the simple types of closed lambda terms or combinators can be interpreted as the theorems of intuitionistic implicational logic . Venneri, using an equivalence between the intersection type system for lambda calculus, without the universal type ω, TA∧λ, and a similar system for combinators, TA∧, shows that the types of TA∧λ are the theorems of a Hilbert-style sublogic of the → ∧ fragment of H→.In this paper we fill a gap in the equivalence proof and (...)
    Direct download (2 more)  
     
    Export citation  
     
    My bibliography  
  9.  1
    Weaker D-Complete Logics.Norman Megill & Martin Bunder - 1996 - Logic Journal of the IGPL 4 (2):215-225.
    BB′IW logic (or T→ is known to be D-complete. This paper shows that there are infinitely many weaker D-complete logics and it also examines how certain D-incomplete logics can be made complete by altering their axioms using simple substitutions.
    Direct download (2 more)  
     
    Export citation  
     
    My bibliography  
  10. Australasian Association for Logic 30th Anniversary Conference.Martin Bunder & Ross T. Brady - 1996 - Bulletin of Symbolic Logic 2 (2):112.
  11. Australasian Association for Logic 31st Annual Conference.Martin Bunder - 1997 - Bulletin of Symbolic Logic 3 (3):363-366.
  12. Australasian Association for Logic 30th Anniversary Conference.Martin Bunder - 1996 - Bulletin of Symbolic Logic 2 (1):112-120.
  13. Intersection Type Systems and Logics Related to the Meyer-Routley System B+.Martin Bunder - 2003 - Australasian Journal of Philosophy 1:43-55.
    Some, but not all, closed terms of the lambda calculus have types; these types are exactly the theorems of intuitionistic implicational logic. An extension of these simple types to intersection types allows all closed lambda terms to have types. The corresponding →∧ logic, related to the Meyer-Routley minimal logic B+ , is weaker than the →∧ fragment of intuitionistic logic. In this paper we provide an introduction to the above work and also determine the →∧ logics that correspond to certain (...)
     
    Export citation  
     
    My bibliography  
  14. Intersection Type Systems and Logics Related to the Meyer–Routley System B+.Martin Bunder - 2003 - Australasian Journal of Logic 1 (2).
    Some, but not all, closed terms of the lambda calculus have types; these types are exactly the theorems of intuitionistic implicational logic. An extension of these simple types to intersection types allows all closed lambda terms to have types. The corresponding →∧ logic, related to the Meyer–Routley minimal logic B+, is weaker than the →∧ fragment of intuitionistic logic. In this paper we provide an introduction to the above work and also determine the →∧ logics that correspond to certain interesting (...)
    Direct download  
     
    Export citation  
     
    My bibliography  
  15. Pure Type Systems with More Liberal Rules.Martin Bunder & Wil Dekkers - 2001 - Journal of Symbolic Logic 66 (4):1561-1580.
    Pure Type Systems, PTSs, introduced as a generalisation of the type systems of Barendregt's lambda-cube, provide a foundation for actual proof assistants, aiming at the mechanic verification of formal proofs. In this paper we consider simplifications of some of the rules of PTSs. This is of independent interest for PTSs as this produces more flexible PTS-like systems, but it will also help, in a later paper, to bridge the gap between PTSs and systems of Illative Combinatory Logic. First we consider (...)
    Direct download  
     
    Export citation  
     
    My bibliography  
  16. Rough Consequence and Other Modal Logics.Martin Bunder - 2015 - Australasian Journal of Logic 12 (1).
    Chakraborty and Banerjee have introduced a rough consequence logic based on the modal logic S5. This paper shows that rough consequence logics, with many of the same properties, can be based on modal logics as weak as K, with a simpler formulation than that of Chakraborty and Banerjee. Also provided are decision procedures for the rough consequence logics and equivalences and independence relations between various systems S and the rough consequence logics, based on them. It also shows that each logic, (...)
    Direct download  
     
    Export citation  
     
    My bibliography  
  17. Completeness of the Propositions-as-Types Interpretation of Intuitionistic Logic Into Illative Combinatory Logic.Wil Dekkers, Martin Bunder & Henk Barendregt - 1998 - Journal of Symbolic Logic 63 (3):869-890.
    Illative combinatory logic consists of the theory of combinators or lambda calculus extended by extra constants intended to capture inference. In a preceding paper, [2], we considered 4 systems of illative combinatory logic that are sound for first order intuitionistic propositional and predicate logic. The interpretation from ordinary logic into the illative systems can be done in two ways: following the propositions-as-types paradigm, in which derivations become combinators, or in a more direct way, in which derivations are not translated. Both (...)
    Direct download  
     
    Export citation  
     
    My bibliography  
  18. 1992 Annual Meeting of the Australasian Association for Logic.John Slaney & Martin W. Bunder - 1993 - Journal of Symbolic Logic 58 (4):1477-1484.