Switch to: References

Add citations

You must login to add citations.
  1. Higher-Order Multi-Valued Resolution.Michael Kohlhase - 1999 - Journal of Applied Non-Classical Logics 9 (4):455-477.
    ABSTRACT This paper introduces a multi-valued variant of higher-order resolution and proves it correct and complete with respect to a variant of Henkin's general model semantics. This resolution method is parametric in the number of truth values as well as in the particular choice of the set of connectives (given by arbitrary truth tables) and even substitutional quantifiers. In the course of the completeness proof we establish a model existence theorem for this logical system. The work reported in this paper (...)
    Direct download (3 more)  
     
    Export citation  
     
    Bookmark   2 citations  
  • A Logic for Describing, Not Verifying, Software.David Lorge Parnas - 1995 - Erkenntnis 43 (3):321 - 338.
    An important perquisite for verification of the correctness of software is the ability to write mathematically precise documents that can be read by practitioners and advanced users. Without such documents, we won't know what properties we should verify. Tabular expressions, in which predicate expressions may appear, have been found useful for this purpose. We frequently use partial functions in our tabular documentation. Conventional interpretations of expressions that describe predicates are not appropriate for our application because they do not deal with (...)
    Direct download (4 more)  
     
    Export citation  
     
    Bookmark  
  • Reasoning About Partial Functions with the Aid of a Computer.William M. Farmer - 1995 - Erkenntnis 43 (3):279 - 294.
    Partial functions are ubiquitous in both mathematics and computer science. Therefore, it is imperative that the underlying logical formalism for a general-purpose mechanized mathematics system provide strong support for reasoning about partial functions. Unfortunately, the common logical formalisms — first-order logic, type theory, and set theory — are usually only adequate for reasoning about partial functionsin theory. However, the approach to partial functions traditionally employed by mathematicians is quite adequatein practice. This paper shows how the traditional approach to partial functions (...)
    Direct download (5 more)  
     
    Export citation  
     
    Bookmark   1 citation  
  • A Tableau Calculus for Partial Functions.Manfred Kerber Michael Kohlhase - unknown
    Even though it is not very often admitted, partial functions do play a significant role in many practical applications of deduction systems. Kleene has already given a semantic account of partial functions using a three-valued logic decades ago, but there has not been a satisfactory mechanization. Recent years have seen a thorough investigation of the framework of many-valued truth-functional logics. However, strong Kleene logic, where quantification is restricted and therefore not truthfunctional, does not fit the framework directly. We solve this (...)
    Direct download  
    Translate
     
     
    Export citation  
     
    Bookmark   1 citation  
  • Many-Valued Logic, Partiality, and Abstraction in Formal Specification Languages.Reiner Hähnle - 2005 - Logic Journal of the IGPL 13 (4):415-433.
    The purpose of this article is to clarify the role that many-valued logic can or should play in formal specification of software systems for modeling partiality. We analyse a representative set of specification languages. Our findings suggest that many-valued logic is less useful for modeling those aspects of partiality, for which it is traditionally intended: modeling non-termination and error values. On the other hand, many-valued logic is emerging as a mainstream tool in abstraction of formal analyses of various kinds, and (...)
    Direct download (3 more)  
     
    Export citation  
     
    Bookmark  
  • A Mechanization of Strong Kleene Logic for Partial Functions.Manfred Kerber Michael Kohlhase - unknown
    Even though it is not very often admitted, partial functions do play a significant role in many practical applications of deduction systems. Kleene has already given a semantic account of partial functions using three-valued logic decades ago, but there has not been a satisfactory mechanization. Recent years have seen a thorough investigation of the framework of many-valued truth-functional logics. However, strong Kleene logic, where quantification is restricted and therefore not truthfunctional, does not fit the framework directly. We solve this problem (...)
    Translate
     
     
    Export citation  
     
    Bookmark   3 citations  
  • The Seven Virtues of Simple Type Theory.William M. Farmer - 2008 - Journal of Applied Logic 6 (3):267-286.
  • A Simple Type Theory with Partial Functions and subtypes11Supported by the MITRE-Sponsored Research Program. Presented at the 9th International Congress of Logic, Methodology and Philosophy of Science Held in Uppsala, Sweden, August 7-14, 1991. [REVIEW]William M. Farmer - 1993 - Annals of Pure and Applied Logic 64 (3):211-240.
    Simple type theory is a higher-order predicate logic for reasoning about truth values, individuals, and simply typed total functions. We present in this paper a version of simple type theory, called PF*, in which functions may be partial and types may have subtypes. We define both a Henkin-style general models semantics and an axiomatic system for PF*, and we prove that the axiomatic system is complete with respect to the general models semantics. We also define a notion of an interpretation (...)
    Direct download (4 more)  
     
    Export citation  
     
    Bookmark   2 citations  
  • Eq-Algebra-Based Fuzzy Type Theory And Its Extensions.Vilém Novák - 2011 - Logic Journal of the IGPL 19 (3):512-542.
    In this paper, we introduce a new algebra called ‘EQ-algebra’, which is an alternative algebra of truth values for formal fuzzy logics. It is specified by replacing implication as the main operation with a fuzzy equality. Namely, EQ-algebra is a semilattice endowed with a binary operation of fuzzy equality and a binary operation of multiplication. Implication is derived from the fuzzy equality and it is not a residuation with respect to multiplication. Consequently, EQ-algebras overlap with residuated lattices but are not (...)
    Direct download (3 more)  
     
    Export citation  
     
    Bookmark   1 citation