10 found
Sort by:
Disambiguations:
Martin Bunder [8]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 & 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  
  3. 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  
  4. 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 (...)
    No categories
    Direct download (4 more)  
     
    My bibliography  
     
    Export citation  
  5. Martin Bunder (1997). Australasian Association for Logic 31st Annual Conference. Bulletin of Symbolic Logic 3 (3):363-366.
    Direct download  
     
    My bibliography  
     
    Export citation  
  6. Martin Bunder & Ross T. Brady (1996). Australasian Association for Logic 30th Anniversary Conference. Bulletin of Symbolic Logic 2:112.
     
    My bibliography  
     
    Export citation  
  7. 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  
  8. 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  
  9. 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  
     
    My bibliography  
     
    Export citation  
  10. 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