4 found
Sort by:
  1. Martin Hofmann, Emanuel Kitzelmann & Ute Schmid (2009). A Unifying Framework for Analysis and Evaluation of Inductive Programming Systems. In B. Goertzel, P. Hitzler & M. Hutter (eds.), Proceedings of the Second Conference on Artificial General Intelligence. Atlantis Press.
    No categories
    Direct download  
     
    My bibliography  
     
    Export citation  
  2. Stephen Bellantoni & Martin Hofmann (2002). A New "Feasible" Arithmetic. Journal of Symbolic Logic 67 (1):104-116.
    A classical quantified modal logic is used to define a "feasible" arithmetic A 1 2 whose provably total functions are exactly the polynomial-time computable functions. Informally, one understands $\Box\alpha$ as "α is feasibly demonstrable". A 1 2 differs from a system A 2 that is as powerful as Peano Arithmetic only by the restriction of induction to ontic (i.e., $\Box$ -free) formulas. Thus, A 1 2 is defined without any reference to bounding terms, and admitting induction over formulas having arbitrarily (...)
    Direct download (6 more)  
     
    My bibliography  
     
    Export citation  
  3. Martin Hofmann (2000). Safe Recursion with Higher Types and BCK-Algebra. Annals of Pure and Applied Logic 104 (1-3):113-166.
    In previous work the author has introduced a lambda calculus SLR with modal and linear types which serves as an extension of Bellantoni–Cook's function algebra BC to higher types. It is a step towards a functional programming language in which all programs run in polynomial time. In this paper we develop a semantics of SLR using BCK -algebras consisting of certain polynomial-time algorithms. It will follow from this semantics that safe recursion with arbitrary result type built up from N and (...)
    Direct download (3 more)  
     
    My bibliography  
     
    Export citation  
  4. Martin Hofmann (1997). An Application of Category-Theoretic Semantics to the Characterisation of Complexity Classes Using Higher-Order Function Algebras. Bulletin of Symbolic Logic 3 (4):469-486.
    We use the category of presheaves over PTIME-functions in order to show that Cook and Urquhart's higher-order function algebra PV ω defines exactly the PTIME-functions. As a byproduct we obtain a syntax-free generalisation of PTIME-computability to higher types. By restricting to sheaves for a suitable topology we obtain a model for intuitionistic predicate logic with ∑ 1 b -induction over PV ω and use this to re-establish that the provably total functions in this system are polynomial time computable. Finally, we (...)
    Direct download (7 more)  
     
    My bibliography  
     
    Export citation