15 found
Order:
Disambiguations
Martin Bunder [17]Martin W. Bunder [2]
  1.  53
    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  
     
    Bookmark   5 citations  
  2.  35
    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 (5 more)  
     
    Export citation  
     
    Bookmark   3 citations  
  3.  23
    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 (8 more)  
     
    Export citation  
     
    Bookmark   2 citations  
  4.  47
    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  
     
    Bookmark   2 citations  
  5.  7
    Australasian association for logic 30th anniversary conference.Martin Bunder & Ross T. Brady - 1996 - Bulletin of Symbolic Logic 2 (2):112.
  6.  6
    Australasian Association for Logic 31st Annual Conference.Martin Bunder - 1997 - Bulletin of Symbolic Logic 3 (3):363-366.
  7.  14
    Australasian Association for Logic 30th Anniversary Conference.Martin Bunder - 1996 - Bulletin of Symbolic Logic 2 (1):112-120.
  8.  25
    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.
  9.  5
    E-mail:.][・, ヲ, ィ ァ ゥ・ ヲ ヲ・ ヲ ヲ・[!"# ァ $" &%'ァ (!%.Martin Bunder - 2004 - Bulletin of Symbolic Logic 10 (3).
    Direct download  
     
    Export citation  
     
    Bookmark  
  10.  51
    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 (8 more)  
     
    Export citation  
     
    Bookmark  
  11.  1
    Rough Consequence and other Modal Logics.Martin Bunder - 2015 - Australasian Journal of Logic 14 (3).
    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  
     
    Bookmark  
  12.  10
    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 (3 more)  
     
    Export citation  
     
    Bookmark  
  13.  6
    1992 Annual Meeting of the Australasian Association for Logic.John Slaney & Martin W. Bunder - 1993 - Journal of Symbolic Logic 58 (4):1477-1484.
  14. 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 (...)
     
    Export citation  
     
    Bookmark   1 citation  
  15. 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 (...)
     
    Export citation  
     
    Bookmark