101 found
Sort by:
Disambiguations:
Melvin Fitting [99]Melvin C. Fitting [3]
  1. Melvin Fitting, Justification Logic.
    No categories
    Direct download  
     
    My bibliography  
     
    Export citation  
  2. Melvin Fitting, A Program to Compute G¨Odel-L¨Ob Fixpoints.
    odel-L¨ ob computability logic (GL). In order to make things relatively self-contained, I sketch the essential ideas of GL, and discuss the significance of its fixpoint theorem. Then I give the algorithm embodied in the program in a little more detail. It should be emphasized that nothing new is presented here — all the theory and methodology are due to others. The main interest is, in a sense, psychological. The approach taken here has been declared in the literature, more (...)
    No categories
    Translate to English
    | Direct download  
     
    My bibliography  
     
    Export citation  
  3. Melvin Fitting, Bisimulations and Boolean Vectors.
    A modal accessibility relation is just a transition relation, and so can be represented by a {0, 1} valued transition matrix. Starting from this observation, I first show that the machinery of matrices, over Boolean algebras more general than the two-valued one, is appropriate for investigating multi-modal semantics. Then I show that bisimulations have a rather elegant theory, when expressed in terms of transformations on Boolean vector spaces. The resulting theory is a curious hybrid, fitting between conventional modal semantics and (...)
    No categories
    Translate to English
    | Direct download  
     
    My bibliography  
     
    Export citation  
  4. Melvin Fitting, Bilattices and the Semantics of Logic Programming.
    Bilattices, due to M. Ginsberg, are a family of truth value spaces that allow elegantly for missing or conflicting information. The simplest example is Belnap’s four-valued logic, based on classical two-valued logic. Among other examples are those based on finite many-valued logics, and on probabilistic valued logic. A fixed point semantics is developed for logic programming, allowing any bilattice as the space of truth values. The mathematics is little more complex than in the classical two-valued setting, but the result provides (...)
    No categories
    Translate to English
    | Direct download  
     
    My bibliography  
     
    Export citation  
  5. Melvin Fitting, Bilattices In Logic Programming.
    Bilattices, introduced by M. Ginsberg, constitute an elegant family of multiple-valued logics. Those meeting certain natural conditions have provided the basis for the semantics of a family of logic programming languages. Now we consider further restrictions on bilattices, to narrow things down to logic programming languages that can, at least in principle, be implemented. Appropriate bilattice background information is presented, so the paper is relatively self-contained.
    No categories
    Translate to English
    | Direct download  
     
    My bibliography  
     
    Export citation  
  6. Melvin Fitting, Databases and Higher Types.
    Generalized databases will be examined, in which attributes can be sets of attributes, or sets of sets of attributes, and other higher type constructs. A precise semantics will be developed for such databases, based on a higher type modal/intensional logic.
    No categories
    Translate to English
    | Direct download  
     
    My bibliography  
     
    Export citation  
  7. Melvin Fitting, Destructive Modal Resolution ∗.
    We present non-clausal resolution systems for propositional modal logics whose Kripke models do not involve symmetry, and for first order versions whose Kripke models do not involve constant domains. We give systems for K, T , K4 and S4; other logics are also possible. Our systems do not require preliminary reduction to a normal form and, in the first order case, intermingle resolution steps with Skolemization steps.
    No categories
    Translate to English
    | Direct download  
     
    My bibliography  
     
    Export citation  
  8. Melvin Fitting, Fixpoint Semantics for Logic Programming A Survey.
    The variety of semantical approaches that have been invented for logic programs is quite broad, drawing on classical and many-valued logic, lattice theory, game theory, and topology. One source of this richness is the inherent non-monotonicity of its negation, something that does not have close parallels with the machinery of other programming paradigms. Nonetheless, much of the work on logic programming semantics seems to exist side by side with similar work done for imperative and functional programming, with relatively minimal contact (...)
    No categories
    Translate to English
    | Direct download  
     
    My bibliography  
     
    Export citation  
  9. Melvin Fitting, Higher-Order Modal Logic—A Sketch.
    First-order modal logic, in the usual formulations, is not suf- ficiently expressive, and as a consequence problems like Frege’s morning star/evening star puzzle arise. The introduction of predicate abstraction machinery provides a natural extension in which such difficulties can be addressed. But this machinery can also be thought of as part of a move to a full higher-order modal logic. In this paper we present a sketch of just such a higher-order modal logic: its formal semantics, and a proof procedure (...)
    Translate to English
    | Direct download  
     
    My bibliography  
     
    Export citation  
  10. Melvin Fitting, Herbrand's Theorem for a Modal Logic.
    Herbrand’s theorem is a central fact about classical logic, [9, 10]. It provides a constructive method for associating, with each first-order formula X, a sequence of formulas X1, X2, X3, . . . , so that X has a first-order proof if and only if some Xi is a tautology. Herbrand’s theorem serves as a constructive alternative to..
    Translate to English
    | Direct download  
     
    My bibliography  
     
    Export citation  
  11. Melvin Fitting, Intensional Logic — Beyond First Order.
    Classical first-order logic can be extended in two different ways to serve as a foundation for mathematics: introduce higher orders, type theory, or introduce sets. As it happens, both approaches have natural analogs for quantified modal logics, both approaches date from the 1960’s, one is not very well-known, and the other is well-known as something else. I will present the basic semantic ideas of both higher order intensional logic, and intensional set theory. Before doing so, I’ll quickly sketch some necessary (...)
    Translate to English
    | Direct download  
     
    My bibliography  
     
    Export citation  
  12. Melvin Fitting, leanTAP Revisited.
    A sequent calculus of a new sort is extracted from the Prolog program leanTAP. This calculus is sound and complete, even though it lacks almost all structural rules. Thinking of leanTAP as a sequent calculus provides a new perspective on it and, in some ways, makes it easier to understand. It is also easier to verify correctness and completeness of the Prolog implementation. In addition, it suggests extensions to other logics, some of which are considered here.
    No categories
    Translate to English
    | Direct download  
     
    My bibliography  
     
    Export citation  
  13. Melvin Fitting, Modality and Databases.
    Two things are done in this paper. First, a modal logic in which one can quantify over both objects and concepts is presented; a semantics and a tableau system are given. It is a natural modal logic, extending standard versions, and capable of addressing several well-known philosophical difficulties successfully. Second, this modal logic is used to introduce a rather different way of looking at relational databases. The idea is to treat records as possible worlds, record entries as objects, and attributes (...)
    No categories
    Translate to English
    | Direct download  
     
    My bibliography  
     
    Export citation  
  14. Melvin Fitting, Modal Logics A Summary of the Well-Behaved.
    Modal logic is an enormous subject, and so any discussion of it must limit itself according to some set of principles. Modal logic is of interest to mathematicians, philosophers, linguists and computer scientists, for somewhat different reasons. Typically a philosopher may be interested in capturing some aspect of necessary truth, while a mathematician may be interested in characterizing a class of models having special structural features. For a computer scientist there is another criterion that is not as relevant for the (...)
    Translate to English
    | Direct download  
     
    My bibliography  
     
    Export citation  
  15. Melvin Fitting, Modal Logics Between Propositional and First Order.
    One can add the machinery of relation symbols and terms to a propositional modal logic without adding quantifiers. Ordinarily this is no extension beyond the propositional. But if terms are allowed to be non-rigid, a scoping mechanism (usually written using lambda abstraction) must also be introduced to avoid ambiguity. Since quantifiers are not present, this is not really a first-order logic, but it is not exactly propositional either. For propositional logics such as K, T and D, adding such machinery produces (...)
    Translate to English
    | Direct download  
     
    My bibliography  
     
    Export citation  
  16. Melvin Fitting, Modal Logic Should Say More Than It Does.
    First-order modal logics, as traditionally formulated, are not expressive enough. It is this that is behind the difficulties in formulating a good analog of Herbrand’s Theorem, as well as the well-known problems with equality, non-rigid designators, definite descriptions, and nondesignating terms. We show how all these problems disappear when modal language is made more expressive in a simple, natural way. We present a semantic tableaux system for the enhanced logic, and (very) briefly discuss implementation issues.
    Translate to English
    | Direct download  
     
    My bibliography  
     
    Export citation  
  17. Melvin Fitting, Metric Methods Three Examples and a Theorem.
    £ The existence of a model for a logic program is generally established by lattice-theoretic arguments. We present three examples to show that metric methods can often be used instead, generally in a direct, straightforward way. One example is a game program, which is not stratified or locally stratified, but which has a unique supported model whose existence is easily established using metric methods. The second example is a program without a unique supported model, but having a part that is (...)
    No categories
    Translate to English
    | Direct download  
     
    My bibliography  
     
    Export citation  
  18. Melvin Fitting, Negation As Refutation.
    A refutation mechanism is introduced into logic programming, dual to the usual proof mechanism; then negation is treated via refutation. A four-valued logic is appropriate for the semantics: true, false, neither, both. Inconsistent programs are allowed, but inconsistencies remain localized. The four-valued logic is a well-known one, due to Belnap, and is the simplest example of Ginsberg’s bilattice notion. An efficient implementation based on semantic tableaux is sketched; it reduces to SLD resolution when negations are not involved. The resulting system (...)
    No categories
    Translate to English
    | Direct download  
     
    My bibliography  
     
    Export citation  
  19. Melvin Fitting, On Quantified Modal Logic.
    Propositional modal logic is a standard tool in many disciplines, but first-order modal logic is not. There are several reasons for this, including multiplicity of versions and inadequate syntax. In this paper we sketch a syntax and semantics for a natural, well-behaved version of first-order modal logic, and show it copes easily with several familiar difficulties. And we provide tableau proof rules to go with the semantics, rules that are, at least in principle, automatable.
    Translate to English
    | Direct download  
     
    My bibliography  
     
    Export citation  
  20. Melvin Fitting, Resolution for Intuitionistic Logic.
    Most automated theorem provers have been built around some version of resolution [4]. But resolution is an inherently Classical logic technique. Attempts to extend the method to other logics have tended to obscure its simplicity. In this paper we present a resolution style theorem prover for Intuitionistic logic that, we believe, retains many of the attractive features of Classical resolution. It is, of course, more complicated, but the complications can be given intuitive motivation. We note that a small change in (...)
    Translate to English
    | Direct download  
     
    My bibliography  
     
    Export citation  
  21. Melvin Fitting, Tableaus for Logic Programming.
    We present a logic programming language, which we call Proflog, with an operational semantics based on tableaus, and a denotational semantics based on supervaluations. We show the two agree. Negation is well-behaved, and semantic non-computability issues do not arise. This is accomplished essentially by dropping a domain closure requirement. The cost is that intuitions developed through the use of classical logic may need modification, though the system is still classical at a level once removed. Implementation problems are discussed very briefly (...)
    No categories
    Translate to English
    | Direct download  
     
    My bibliography  
     
    Export citation  
  22. Melvin Fitting, The Family of Stable Models.
    The family of all stable models for a logic program has a surprisingly simple overall structure, once two naturally occurring orderings are made explicit. In a so-called knowledge ordering based on degree of definedness, every logic program P has a smallest stable model, sk P — it is the well-founded model. There is also a dual largest stable model, S k P, which has not been considered before. There is another ordering based on degree of truth. Taking the meet and (...)
    No categories
    Translate to English
    | Direct download  
     
    My bibliography  
     
    Export citation  
  23. Melvin C. Fitting, Well-Founded Semantics, Generalized.
    Classical fixpoint semantics for logic programs is based on the TP immediate consequence operator. The Kripke/Kleene, three-valued, semantics uses ΦP, which extends TP to Kleene’s strong three-valued logic. Both these approaches generalize to cover logic programming systems based on a wide class of logics, provided only that the underlying structure be that of a bilattice. This was presented in earlier papers. Recently well-founded semantics has become influential for classical logic programs. We show how the well-founded approach also extends naturally to (...)
    No categories
    Translate to English
    | Direct download  
     
    My bibliography  
     
    Export citation  
  24. Melvin Fitting & Marion Ben-Jacob, Stratified, Weak Stratified, and Three-Valued Semantics.
    We investigate the relationship between three-valued Kripke/Kleene semantics and stratified semantics for stratifiable logic programs. We first show these are compatible, in the sense that if the three-valued semantics assigns a classical truth value, the stratified approach will assign the same value. Next, the familiar fixed point semantics for pure Horn clause programs gives both smallest and biggest fixed points fundamental roles. We show how to extend this idea to the family of stratifiable logic programs, producing a semantics we call (...)
    No categories
    Translate to English
    | Direct download  
     
    My bibliography  
     
    Export citation  
  25. Melvin Fitting, A Logic of Explicit Knowledge.
    A well-known problem with Hintikka-style logics of knowledge is that of logical omniscience. One knows too much. This breaks down into two subproblems: one knows all tautologies, and one’s knowledge is closed under consequence. A way of addressing the second of these is to move from knowledge simpliciter, to knowledge for a reason. Then, as consequences become ‘further away’ from one’s basic knowledge, reasons for them become more complex, thus providing a kind of resource measurement. One kind of reason is (...)
    Translate to English
    | Direct download  
     
    My bibliography  
     
    Export citation  
  26. Melvin Fitting, Explicit Logics of Knowledge and Conservativity.
    Several justification logics have evolved, starting with the logicLP, (Artemov 2001). These can be thought of as explicit versions of modal logics, or logics of knowledge or belief, in which the unanalyzed necessity (knowledge, belief) operator has been replaced with a family of explicit justification terms. Modal logics come in various strengths. For their corresponding justification logics, differing strength is reflected in different vocabularies. What we show here is that for justification logics corresponding to modal logics extending T, various familiar (...)
    Translate to English
    | Direct download  
     
    My bibliography  
     
    Export citation  
  27. Melvin Fitting, Justification Logics and Hybrid Logics.
    Hybrid logics internalize their own semantics. Members of the newer family of justification logics internalize their own proof methodology. It is an appealing goal to combine these two ideas into a single system, and in this paper we make a start. We present a hybrid/justification version of the modal logic T. We give a semantics, a proof theory, and prove a completeness theorem. In addition, we prove a Realization Theorem, something that plays a central role for justification logics generally. Since (...)
    Translate to English
    | Direct download  
     
    My bibliography  
     
    Export citation  
  28. Melvin Fitting, Justification Logics, Logics of Knowledge, and Conservativity.
    Several justification logics have been created, starting with the logic LP, [1]. These can be thought of as explicit versions of modal logics, or of logics of knowledge or belief, in which the unanalyzed necessity (knowledge, belief) operator has been replaced with a family of explicit justification terms. We begin by sketching the basics of justification logics and their relations with modal logics. Then we move to new material. Modal logics come in various strengths. For their corresponding justification logics, differing (...)
    Translate to English
    | Direct download  
     
    My bibliography  
     
    Export citation  
  29. Melvin Fitting, Kleene's Logic, Generalized.
    Kleene’s well-known strong three-valued logic is shown to be one of a family of logics with similar mathematical properties. These logics are produced by an intuitively natural construction. The resulting logics have direct relationships with bilattices. In addition they possess mathematical features that lend themselves well to semantical constructions based on fixpoint procedures, as in logic programming.
    Translate to English
    | Direct download  
     
    My bibliography  
     
    Export citation  
  30. Melvin Fitting, Kleene's Three Valued Logics and Their Children.
    Kleene’s strong three-valued logic extends naturally to a four-valued logic proposed by Belnap. We introduce a guard connective into Belnap’s logic and consider a few of its properties. Then we show that by using it four-valued analogs of Kleene’s weak three-valued logic, and the asymmetric logic of Lisp are also available. We propose an extension of these ideas to the family of distributive bilattices. Finally we show that for bilinear bilattices the extensions do not produce any new equivalences.
    No categories
    Translate to English
    | Direct download  
     
    My bibliography  
     
    Export citation  
  31. Melvin Fitting, Many-Valued Modal Logics II.
    Suppose there are several experts, with some dominating others (expert A dominates expert B if B says something is true whenever A says it is). Suppose, further, that each of the experts has his or her own view of what is possible — in other words each of the experts has their own Kripke model in mind (subject, of course, to the dominance relation that may hold between experts). How will they assign truth values to sentences in a common modal (...)
    Translate to English
    | Direct download (2 more)  
     
    My bibliography  
     
    Export citation  
  32. Melvin Fitting, Many-Valued Non-Monotonic Modal Logics.
    Among non-monotonic systems of reasoning, non-monotonic modal logics, and autoepistemic logic in particular, have had considerable success. The presence of explicit modal operators allows flexibility in the embedding of other approaches. Also several theoretical results of interest have been established concerning these logics. In this paper we introduce non-monotonic modal logics based on many-valued logics, rather than on classical logic. This extends earlier work of ours on many-valued modal logics. Intended applications are to situations involving several reasoners, not just one (...)
    Translate to English
    | Direct download  
     
    My bibliography  
     
    Export citation  
  33. Melvin Fitting, Possible World Semantics for First Order Lp.
    First we have individual variables, as usual in first-order logics. (We do not have individual constants, but this is a minor point.) The propositional logic LP has justification constants, but in FOLP these are generalized to allow individual variables as arguments. Thus we have as justification constants c, c(x), c(x, y), . . . . Similarly LP has justification variables, but in FOLP these can be parametrized with individual variables p, p(x), p(x, y), . . . . To keep terminology (...)
    Translate to English
    | Direct download  
     
    My bibliography  
     
    Export citation  
  34. Melvin Fitting, Reasoning with Justifications.
    This is an expository paper in which the basic ideas of a family of Justification Logics are presented. Justification Logics evolved from a logic called LP, introduced by Sergei Artemov [1, 3], which formed the central part of a project to provide an arithmetic semantics for propositional intuitionistic logic. The project was successful, but there was a considerable bonus: LP came to be understood as a logic of knowledge with explicit justifications and, as such, was capable of addressing in a (...)
    No categories
    Translate to English
    | Direct download  
     
    My bibliography  
     
    Export citation  
  35. Melvin Fitting, S4lp and Local Realizability.
    The logic S4LP combines the modal logic S4 with the justification logic LP, both axiomatically and semantically. We introduce a simple restriction on the behavior of constants in S4LP, having no effect on the LP sublogic. Under this restriction some powerful derived rules are established. Then these are used to show completeness relative to a semantics having what we call the local realizability property: at each world and for each formula true at that world there is a realization also true (...)
    Translate to English
    | Direct download  
     
    My bibliography  
     
    Export citation  
  36. Melvin Fitting, The Realization Theorem for S5 a Simple, Constructive Proof.
    Justification logics are logics of knowledge in which explicit reasons are formally represented. Standard logics of knowledge have justification logic analogs. Connecting justification logics and logics of knowledge are Realization Theorems. In this paper we give a new, constructive proof of the Realization Theorem connecting S5 and its justification analog, JS5. This proof is, I believe, the simplest in the literature.
    Translate to English
    | Direct download  
     
    My bibliography  
     
    Export citation  
  37. Melvin C. Fitting, Many-Valued Modal Logics.
    Two families of many-valued modal logics are investigated. Semantically, one family is characterized using Kripke models that allow formulas to take values in a finite many-valued logic, at each possible world. The second family generalizes this to allow the accessibility relation between worlds also to be many-valued. Gentzen sequent calculi are given for both versions, and soundness and completeness are established.
    Translate to English
    | Direct download (2 more)  
     
    My bibliography  
     
    Export citation  
  38. Melvin Fitting (2014). Nested Sequents for Intuitionistic Logics. Notre Dame Journal of Formal Logic 55 (1):41-61.
    Direct download (2 more)  
     
    My bibliography  
     
    Export citation  
  39. Melvin Fitting (2014). Possible World Semantics for First-Order Logic of Proofs. Annals of Pure and Applied Logic 165 (1):225-240.
    Direct download (2 more)  
     
    My bibliography  
     
    Export citation  
  40. Anil Nerode & Melvin Fitting (2014). The Life and Work of Sergei Artemov. Annals of Pure and Applied Logic 165 (1):3-5.
    No categories
    Direct download (2 more)  
     
    My bibliography  
     
    Export citation  
  41. Melvin Fitting (2012). Barcan Both Ways. Journal of Applied Non-Classical Logics 9 (2-3):329-344.
    No categories
    Direct download (6 more)  
     
    My bibliography  
     
    Export citation  
  42. Melvin Fitting (2012). Prefixed Tableaus and Nested Sequents. Annals of Pure and Applied Logic 163 (3):291 - 313.
    Nested sequent systems for modal logics are a relatively recent development, within the general area known as deep reasoning. The idea of deep reasoning is to create systems within which one operates at lower levels in formulas than just those involving the main connective or operator. Prefixed tableaus go back to 1972, and are modal tableau systems with extra machinery to represent accessibility in a purely syntactic way. We show that modal nested sequents and prefixed modal tableaus are notational variants (...)
    Direct download (5 more)  
     
    My bibliography  
     
    Export citation  
  43. Melvin Fitting (2012). Torben Braüner, Hybrid Logic and its Proof-Theory, Applied Logic Series Volume 37, Springer, 2011, Pp. XIII+231. ISBN: 978-94-007-0001-7 (Hardcover) EURO 99,95, ISBN: 978-94-007-0002-4 (eBook) EURO 99,99. [REVIEW] Studia Logica 100 (5):1051-1053.
    Direct download (5 more)  
     
    My bibliography  
     
    Export citation  
  44. Melvin Fitting (2011). Reasoning About Games. Studia Logica 99 (1-3):143-169.
    is used to give a formalization of Artemov’s knowledge based reasoning approach to game theory, (KBR), [ 4 , 5 ]. Epistemic states of players are represented explicitly and reasoned about formally. We give a detailed analysis of the Centipede game using both proof theoretic and semantic machinery. This helps make the case that PDL + E can be a useful basis for the logical investigation of game theory.
    Direct download (7 more)  
     
    My bibliography  
     
    Export citation  
  45. Melvin Fitting (2009). How True It is = Who Says It's True. Studia Logica 91 (3):335 - 366.
    This is a largely expository paper in which the following simple idea is pursued. Take the truth value of a formula to be the set of agents that accept the formula as true. This means we work with an arbitrary (finite) Boolean algebra as the truth value space. When this is properly formalized, complete modal tableau systems exist, and there are natural versions of bisimulations that behave well from an algebraic point of view. There remain significant problems concerning the proper (...)
    Direct download (5 more)  
     
    My bibliography  
     
    Export citation  
  46. Melvin Fitting (2009). Realizations and LP. Annals of Pure and Applied Logic 161 (3):368-387.
    No categories
    Direct download (4 more)  
     
    My bibliography  
     
    Export citation  
  47. Melvin Fitting (2008). A Quantified Logic of Evidence. Annals of Pure and Applied Logic 152 (1):67-83.
    No categories
    Direct download (4 more)  
     
    My bibliography  
     
    Export citation  
  48. Melvin Fitting, Intensional Logic. Stanford Encyclopedia of Philosophy.
    There is an obvious difference between what a term designates and what it means. At least it is obvious that there is a difference. In some way, meaning determines designation, but is not synonymous with it. After all, “the morning star” and “the evening star” both designate the planet Venus, but don't have the same meaning. Intensional logic attempts to study both designation and meaning and investigate the relationships between them.
    Direct download  
     
    My bibliography  
     
    Export citation  
  49. Melvin Fitting (2007). Correction to, 84: 1–22, 2006. Studia Logica 85 (2):275-275.
    No categories
    Direct download  
     
    My bibliography  
     
    Export citation  
  50. Melvin Fitting (2007). Correction to FOIL Axiomatized Studia Logica , 84:1–22, 2006. Studia Logica 85 (2):275 -.
    There is an error in the completeness proof for the {λ, =} part of FOIL-K. The error occurs in Section 4, in the text following the proof of Corollary 4.7, and concerns the definition of the interpretation I on relation symbols. Before this point in the paper, for each object variable v an equivalence class v has been defined, and for each intension variable f a function f has been defined. Then the following definition is given for a relation symbol (...)
    Direct download (6 more)  
     
    My bibliography  
     
    Export citation  
1 — 50 / 101