40 found
Sort by:
  1. M. W. Bunder & R. M. Rizkalla (2009). Proof-Finding Algorithms for Classical and Subclassical Propositional Logics. Notre Dame Journal of Formal Logic 50 (3):261-273.
    The formulas-as-types isomorphism tells us that every proof and theorem, in the intuitionistic implicational logic $H_\rightarrow$, corresponds to a lambda term or combinator and its type. The algorithms of Bunder very efficiently find a lambda term inhabitant, if any, of any given type of $H_\rightarrow$ and of many of its subsystems. In most cases the search procedure has a simple bound based roughly on the length of the formula involved. Computer implementations of some of these procedures were done in Dekker. (...)
    Direct download (3 more)  
     
    My bibliography  
     
    Export citation  
  2. M. W. Bunder & W. J. M. Dekkers (2005). Equivalences Between Pure Type Systems and Systems of Illative Combinatory Logic. Notre Dame Journal of Formal Logic 46 (2):181-205.
    Pure Type Systems, PTSs, were introduced as a generalization of the type systems of Barendregt's lambda cube and were designed to provide a foundation for actual proof assistants which will verify proofs. Systems of illative combinatory logic or lambda calculus, ICLs, were introduced by Curry and Church as a foundation for logic and mathematics. In an earlier paper we considered two changes to the rules of the PTSs which made these rules more like ICL rules. This led to four kinds (...)
    Direct download (8 more)  
     
    My bibliography  
     
    Export citation  
  3. M. W. Bunder (2002). A Classification of Intersection Type Systems. Journal of Symbolic Logic 67 (1):353-368.
    The first system of intersection types, Coppo and Dezani [3], extended simple types to include intersections and added intersection introduction and elimination rules (( $\wedge$ I) and ( $\wedge$ E)) to the type assignment system. The major advantage of these new types was that they were invariant under β-equality, later work by Barendregt, Coppo and Dezani [1], extended this to include an (η) rule which gave types invariant under βη-reduction. Urzyczyn proved in [6] that for both these systems it is (...)
    Direct download (6 more)  
     
    My bibliography  
     
    Export citation  
  4. M. W. Bunder (2000). Expedited Broda-Damas Bracket Abstraction. Journal of Symbolic Logic 65 (4):1850-1857.
    A bracket abstraction algorithm is a means of translating λ-terms into combinators. Broda and Damas, in [1], introduce a new, rather natural set of combinators and a new form of bracket abstraction which introduces at most one combinator for each λ-abstraction. This leads to particularly compact combinatory terms. A disadvantage of their abstraction process is that it includes the whole Schonfinkel [4] algorithm plus two mappings which convert the Schonfinkel abstract into the new abstract. This paper shows how the new (...)
    Direct download (6 more)  
     
    My bibliography  
     
    Export citation  
  5. M. W. Bunder (1995). A Simplified Form of Condensed Detachment. Journal of Logic, Language and Information 4 (2):169-173.
    This paper gives a simple, elegant statement of the condensed detachment rule that is independent of most general unifiers and proves that this is equivalent to the longer, more usual, formulation.
    Direct download (4 more)  
     
    My bibliography  
     
    Export citation  
  6. M. W. Bunder (1990). Some Improvements to Turner's Algorithm for Bracket Abstraction. Journal of Symbolic Logic 55 (2):656-669.
    Direct download (6 more)  
     
    My bibliography  
     
    Export citation  
  7. M. W. Bunder (1988). Arithmetic Based on the Church Numerals in Illative Combinatory Logic. Studia Logica 47 (2):129 - 143.
    In the early thirties, Church developed predicate calculus within a system based on lambda calculus. Rosser and Kleene developed Arithmetic within this system, but using a Godelization technique showed the system to be inconsistent.Alternative systems to that of Church have been developed, but so far more complex definitions of the natural numbers have had to be used. The present paper based on a system of illative combinatory logic developed previously by the author, does allow the use of the Church numerals. (...)
    Direct download (5 more)  
     
    My bibliography  
     
    Export citation  
  8. M. W. Bunder (1987). Some Consistency Proofs and a Characterization of Inconsistency Proofs in Illative Combinatory Logic. Journal of Symbolic Logic 52 (1):89-110.
    Direct download (6 more)  
     
    My bibliography  
     
    Export citation  
  9. M. W. Bunder (1987). Some Generalizations to Two Systems of Set Theory Based on Combinatory Logic. Archive for Mathematical Logic 26 (1):5-12.
    No categories
    Direct download  
     
    My bibliography  
     
    Export citation  
  10. M. W. Bunder (1984). Category Theory Based on Combinatory Logic. Archive for Mathematical Logic 24 (1):1-16.
    No categories
    Direct download  
     
    My bibliography  
     
    Export citation  
  11. M. W. Bunder (1984). Some Definitions of Negation Leading to Paraconsistent Logics. Studia Logica 43 (1-2):75 - 78.
    In positive logic the negation of a propositionA is defined byA X whereX is some fixed proposition. A number of standard properties of negation, includingreductio ad absurdum, can then be proved, but not the law of noncontradiction so that this forms a paraconsistent logic. Various stronger paraconsistent logics are then generated by putting in particular propositions forX. These propositions range from true through contingent to false.
    Direct download (5 more)  
     
    My bibliography  
     
    Export citation  
  12. M. W. Bunder (1983). A Weak Absolute Consistency Proof for Some Systems of Illative Combinatory Logic. Journal of Symbolic Logic 48 (3):771-776.
    Direct download (6 more)  
     
    My bibliography  
     
    Export citation  
  13. M. W. Bunder (1982). Deduction Theorems for Weak Implicational Logics. Studia Logica 41 (2-3):95 - 108.
    The standard deduction theorem or introduction rule for implication, for classical logic is also valid for intuitionistic logic, but just as with predicate logic, other rules of inference have to be restricted if the theorem is to hold for weaker implicational logics.In this paper we look in detail at special cases of the Gentzen rule for and show that various subsets of these in effect constitute deduction theorems determining all the theorems of many well known as well as not well (...)
    Direct download (5 more)  
     
    My bibliography  
     
    Export citation  
  14. M. W. Bunder (1982). Some Results in Aczel‐Feferman Logic and Set Theory. Mathematical Logic Quarterly 28 (19):269-276.
    No categories
    Direct download (3 more)  
     
    My bibliography  
     
    Export citation  
  15. M. W. Bunder (1982). Illative Combinatory Logic Without Equality as a Primitive Predicate. Notre Dame Journal of Formal Logic 23 (1):62-70.
  16. M. W. Bunder (1980). A Note on Quantified Significance Logics. Bulletin of the Section of Logic 9 (4):159-161.
    No categories
    Direct download  
     
    My bibliography  
     
    Export citation  
  17. M. W. Bunder (1980). Significance and Illative Combinatory Logics. Notre Dame Journal of Formal Logic 21 (2):380-384.
    Direct download (4 more)  
     
    My bibliography  
     
    Export citation  
  18. M. W. Bunder (1979). Paraconsistent Combinatory Logic,„. Bulletin of the Section of Logic 8 (4):177-180.
    No categories
    Direct download  
     
    My bibliography  
     
    Export citation  
  19. M. W. Bunder (1979). Alternative Forms of Propositional Calculus for a Given Deduction Theorem. Notre Dame Journal of Formal Logic 20 (3):613-619.
    Direct download (4 more)  
     
    My bibliography  
     
    Export citation  
  20. M. W. Bunder (1979). A More Relevant Relevance Logic. Notre Dame Journal of Formal Logic 20 (3):701-704.
    Direct download (4 more)  
     
    My bibliography  
     
    Export citation  
  21. M. W. Bunder (1979). Deduction Theorems in Significance Logics. Notre Dame Journal of Formal Logic 20 (3):695-700.
    Direct download (4 more)  
     
    My bibliography  
     
    Export citation  
  22. M. W. Bunder (1979). Generalized Restricted Generality. Notre Dame Journal of Formal Logic 20 (3):620-624.
    Direct download (4 more)  
     
    My bibliography  
     
    Export citation  
  23. M. W. Bunder (1979). $\Lambda$-Elimination in Illative Combinatory Logic. Notre Dame Journal of Formal Logic 20 (3):628-630.
    Direct download (3 more)  
     
    My bibliography  
     
    Export citation  
  24. M. W. Bunder (1979). On the Equivalence of Systems of Rules and Systems of Axioms in Illative Combinatory Logic. Notre Dame Journal of Formal Logic 20 (3):603-608.
    Direct download (3 more)  
     
    My bibliography  
     
    Export citation  
  25. M. W. Bunder (1979). Scott's Models and Illative Combinatory Logic. Notre Dame Journal of Formal Logic 20 (3):609-612.
    Direct download (3 more)  
     
    My bibliography  
     
    Export citation  
  26. M. W. Bunder (1979). Variable Binding Term Operators in $\Lambda $-Calculus. Notre Dame Journal of Formal Logic 20 (4):876-878.
  27. M. W. Bunder (1978). Equality In. Mathematical Logic Quarterly 24 (8):125-127.
    No categories
    Direct download (3 more)  
     
    My bibliography  
     
    Export citation  
  28. M. W. Bunder & R. K. Meyer (1978). On the Inconsistency of Systems Similar to F*21. Journal of Symbolic Logic 43 (1):1 - 2.
    Direct download (3 more)  
     
    My bibliography  
     
    Export citation  
  29. M. W. Bunder & R. K. Meyer (1978). On the Inconsistency of Systems Similar to $Mathscr{F}^Ast_{21}$. Journal of Symbolic Logic 43 (1):1-2.
    Direct download (2 more)  
     
    My bibliography  
     
    Export citation  
  30. M. W. Bunder & Jonathan P. Seldin (1978). Some Anomalies in Fitch's System QD. Journal of Symbolic Logic 43 (2):247-249.
    Direct download (6 more)  
     
    My bibliography  
     
    Export citation  
  31. M. W. Bunder (1977). Consistency Notions in Illative Combinatory Logic. Journal of Symbolic Logic 42 (4):527-529.
    Direct download (6 more)  
     
    My bibliography  
     
    Export citation  
  32. M. W. Bunder (1976). The Inconsistency of F*21. Journal of Symbolic Logic 41 (2):467 - 468.
    Direct download (3 more)  
     
    My bibliography  
     
    Export citation  
  33. M. W. Bunder (1976). The Inconsistency of $Mathscr{F}^Ast_{21}$. Journal of Symbolic Logic 41 (2):467-468.
    Direct download (2 more)  
     
    My bibliography  
     
    Export citation  
  34. M. W. Bunder (1976). Some Notes On: ``A Deduction Theorem for Restricted Generality''. Notre Dame Journal of Formal Logic 17 (1):153-154.
    Direct download (2 more)  
     
    My bibliography  
     
    Export citation  
  35. M. W. Bunder (1974). Some Inconsistencies in Illative Combinatory Logic. Mathematical Logic Quarterly 20 (13‐18):199-201.
    No categories
    Direct download (3 more)  
     
    My bibliography  
     
    Export citation  
  36. M. W. Bunder (1974). Propositional and Predicate Calculuses Based on Combinatory Logic. Notre Dame Journal of Formal Logic 15 (1):25-34.
    Direct download (2 more)  
     
    My bibliography  
     
    Export citation  
  37. M. W. Bunder (1974). Various Systems of Set Theory Based on Combinatory Logic. Notre Dame Journal of Formal Logic 15 (2):192-206.
    Direct download (4 more)  
     
    My bibliography  
     
    Export citation  
  38. M. W. Bunder (1973). A Deduction Theorem for Restricted Generality. Notre Dame Journal of Formal Logic 14 (3):341-346.
    Direct download (3 more)  
     
    My bibliography  
     
    Export citation  
  39. M. W. Bunder (1973). A Generalised Kleene-Rosser Paradox for a System Containing the Combinator ${\Bf K}$. Notre Dame Journal of Formal Logic 14 (1):53-54.
    Direct download (3 more)  
     
    My bibliography  
     
    Export citation  
  40. M. W. Bunder (1970). A Paradox in Illative Combinatory Logic. Notre Dame Journal of Formal Logic 11 (4):467-470.
    Direct download (4 more)  
     
    My bibliography  
     
    Export citation