13 found
Sort by:
Disambiguations:
Martin Bunder [11]Martin W. Bunder [2]
  1. Martin Bunder (2004). E-Mail:.][・, ヲ, ィ ァ ゥ・ ヲ ヲ・ ヲ ヲ・[!"# ァ $" &%'ァ (!%. Bulletin of Symbolic Logic 10 (3).
    Direct download  
     
    My bibliography  
     
    Export citation  
  2. Martin Bunder (2003). Intersection Type Systems and Logics Related to the Meyer-Routley System B+. 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 (...)
     
    My bibliography  
     
    Export citation  
  3. Martin Bunder (2002). Intersection Types for Lambda-Terms and Combinators and Their Logics. 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  
     
    My bibliography  
     
    Export citation  
  4. Martin Bunder & Wil Dekkers (2001). Pure Type Systems with More Liberal Rules. 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 (6 more)  
     
    My bibliography  
     
    Export citation  
  5. Wil Dekkers, Martin Bunder & Henk Barendregt (1998). Completeness of the Propositions-as-Types Interpretation of Intuitionistic Logic Into Illative Combinatory Logic. 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 (6 more)  
     
    My bibliography  
     
    Export citation  
  6. Wil Dekkers, Martin Bunder & Henk Barendregt (1998). Completeness of Two Systems of Illative Combinatory Logic for First-Order Propositional and Predicate Calculus. 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)  
     
    My bibliography  
     
    Export citation  
  7. Martin Bunder (1997). Australasian Association for Logic 31st Annual Conference. Bulletin of Symbolic Logic 3 (3):363-366.
    Direct download (2 more)  
     
    My bibliography  
     
    Export citation  
  8. Martin Bunder & Ross T. Brady (1996). Australasian Association for Logic 30th Anniversary Conference. Bulletin of Symbolic Logic 2 (2):112.
    Direct download  
     
    My bibliography  
     
    Export citation  
  9. Norman Megill & Martin Bunder (1996). Weaker D-Complete Logics. 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  
     
    My bibliography  
     
    Export citation  
  10. Martin Bunder (1994). 1993 Annual Meeting of the Australasian Association for Logic, Adelaide, Australia, July 9-11, 1993. Journal of Symbolic Logic 59 (4):1443-1449.
    Direct download (5 more)  
     
    My bibliography  
     
    Export citation  
  11. Henk Barendregt, Martin Bunder & Wil Dekkers (1993). Systems of Illative Combinatory Logic Complete for First-Order Propositional and Predicate Calculus. 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 (7 more)  
     
    My bibliography  
     
    Export citation  
  12. John Slaney & Martin W. Bunder (1993). 1992 Annual Meeting of the Australasian Association for Logic. Journal of Symbolic Logic 58 (4):1477-1484.
    Direct download (2 more)  
     
    My bibliography  
     
    Export citation  
  13. Martin W. Bunder, J. Roger Hindley & Jonathan P. Seldin (1989). On Adding (Ξ) to Weak Equality in Combinatory Logic. 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 (6 more)  
     
    My bibliography  
     
    Export citation