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 (...) strength is reflected in different vocabularies. What we show here is that for justification logics corresponding to modal logics extending T, various familiar extensions are actually conservative with respect to each other. Our method of proof is very simple, and general enough to handle several justification logics not directly corresponding to distinct modal logics. Our methods do not, however, allow us to prove comparable results for justification logics corresponding to modal logics that do not extend T. That is, we are able to handle explicit logics of knowledge, but not explicit logics of belief. This remains open. (shrink)

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.

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 (...) extensions are actually conservative with respect to each other. Our method of proof is very simple, and general enough to handle several justification logics not directly corresponding to distinct modal logics. Our methods do not, however, allow us to prove comparable results for justification logics corresponding to modal logics that do not extend T. That is, we are able to handle explicit logics of knowledge, but not explicit logics of belief. This remains open. (shrink)

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 (...) weak stratified. Finally, we show weak stratified semantics coincides exactly with the three-valued approach on stratifiable programs, though the three-valued version is generally applicable, and does not require stratification assumptions. (shrink)

The badness of having conflicting emotions is a familiar theme in academic ethics, clinical psychology, and commercial self-help, where emotional harmony is often put forward as an ideal. Many philosophers give emotional harmony pride of place in their theories of practical reason.1 Here we offer a defense of a particular species of emotional conflict, namely, ambivalence. We articulate an conception of ambivalence, on which ambivalence is unresolved inconsistent desire (§1) and present a case of appropriate ambivalence (§2), before considering two (...) alternative defenses of emotional conflict (§3). We then argue that inconsistent desires can be fitting (§4) and that it can be reasonable not to resolve inconsistent desires (§5), before considering an objection (§6) and concluding the discussion (§7). (shrink)

Philosophers are now wary of conflating the “fittingness” or accuracy of an emotion with any form of moral assessment of that emotion. Justin D’Arms and Daniel Jacobson, who originally cautioned against this “conflation”, also warned philosophers not to infer that an emotion is inaccurate from the fact that feeling it would be morally inappropriate, or that it is accurate from the fact that feeling it would be morally appropriate. Such inferences, they argue, risk committing “the moralistic fallacy”, a mistake they (...) claim is widespread throughout the work of contemporary and historical moral philosophers. I argue that many basic and familiar forms of moral assessment of the emotions are not subject to these arguments. I illustrate this by reconsidering the idea that to assess an emotion as “fitting” is to assess it as what a virtuous person would feel. After showing how assessments akin to this “virtue-theoretical” notion of fit may be prevalent even outside of the Aristotelian tradition, I suggest some more charitable and philosophically productive interpretations of the philosophical views of the emotions that D’Arms and Jacobson criticize, and argue that we cannot coherently theorize about the fittingness conditions of the emotions in a morally neutral way. (shrink)

Company–cause fit has been one of the major issues in the domain of corporate social responsibility. This study tries to expand the perspective from company–cause to company–non-profit organization (NPO) fit, and it gives implications to firms looking for long-term collaboration with an NPO. Specifically, it suggests three types of fit, i.e., familiarity, business, and activity fit and investigates the potential effects of these fits in social alliances between companies and the partnering NPOs on consumer attributions of the firms’ motives (...) for the alliances. An experiment that used scenarios revealed that consumers perceive high-fitted alliances on the dimensions of the familiarity and activity fit as being more public-serving than low-matched ones. However, the consumers’ attribution of the motive is not different between the high and low business fit. The implications of the research results are discussed from an academic and practical standpoint. (shrink)

Word recognition is the Petri dish of the cognitive sciences. The processes hypothesized to govern naming, identifying and evaluating words have shaped this field since its origin in the 1970s. Techniques to measure lexical processing are not just the back-bone of the typical experimental psychology laboratory, but are now routinely used by cognitive neuroscientists to study brain processing and increasingly by social and clinical psychologists (Eder, Hommel, and De Houwer 2007). Models developed to explain lexical processing have also aspired to (...) be statements about the nature of human cognition (e.g., connectionist models, Plaut, McClelland, Seidenberg, and Patterson 1996). Words were convenient objects to study for cognitive psychologists because they are welldefined and their nature as alphabetic strings was a good fit to analysis with the computer programming languages of the 1970s and 1980s which excelled at string manipulation. But are words actually the privileged unit of mental representation and processing that all of this scientific attention makes them out to be? Like a growing number of other language researchers, our answer is no (see, e.g., (Bybee and Hopper 2001; Wray 2002). We propose that the mental representations for lexical structures form a continuum, from word combinations which have fossilized into single units (nightclub) to those that both exist as independent units and yet have bonds, varying in tightness, with the words with which they frequently co-occur (Harris 1998). The first line of support for this view is the simple observation that fluent speakers easily recognize the familiarity and cohesive quality of word combinations in their language. Examples in English include common noun compounds (last year, brand new), verb phrases (cut down, get a hold of, faced with) and other multi-word expressions such as common sayings and references to cultural concepts (saved by the bell, speed of light; Jackendoff 1995).. (shrink)

It seems trivial to identify sound sequences as music or speech, particularly when the sequences come from different sound sources, such as an orchestra and a human voice. Can we also easily distinguish these categories when the sequence comes from the same sound source? On the basis of which acoustic features? We investigated these questions by examining listeners’ classification of sound sequences performed by an instrument intertwining both speech and music: the dùndún talking drum. The dùndún is commonly used in (...) south-west Nigeria as a musical instrument but is also perfectly fit for linguistic usage in what has been described as speech surrogates in Africa. One hundred seven participants from diverse geographical locations (15 different mother tongues represented) took part in an online experiment. Fifty-one participants reported being familiar with the dùndún talking drum, 55% of those being speakers of Yorùbá. During the experiment, participants listened to 30 dùndún samples of about 7s long, performed either as music or Yorùbá speech surrogate (n= 15 each) by a professional musician, and were asked to classify each sample as music or speech-like. The classification task revealed the ability of the listeners to identify the samples as intended by the performer, particularly when they were familiar with the dùndún, though even unfamiliar participants performed above chance. A logistic regression predicting participants’ classification of the samples from several acoustic features confirmed the perceptual relevance of intensity, pitch, timbre, and timing measures and their interaction with listener familiarity. In all, this study provides empirical evidence supporting the discriminating role of acoustic features and the modulatory role of familiarity in teasing apart speech and music. (shrink)

Purpose This study aims to explore the potential of mobile assistive technology as a vocational tool for blind workers. Specifically, it investigates: Can MAT-enabled BW to perform better at the workplace and will insight into MAT-enabled capabilities impact employer perception regarding BW employability. Design/methodology/approach Exploratory case study which draws on theories of fit to analyze observational and interview data at an organization familiar with employing, training and referring BW. Findings MAT can increase blind worker job fit, positively impacting their performance, (...) self-reliance and managerial perceptions regarding their employability. Research limitations/implications A conceptual framework is articulated which expands current literature on fit to better account for the assistive potential of mobile technology for differently abled workers. Practical implications The positive impact of MAT on managerial perceptions of BW fit and employability can inform the regimes of employers, job skills trainers, vocational rehabilitation specialists and policy makers. Social implications Insights on the use of MAT as a vocational tool can reduce the systemic workplace disenfranchisement of blind people. Originality/value This paper presents novel theory which accounts for the impact of MAT on the job fit of differently abled workers. (shrink)

This is a thorough treatment of first-order modal logic. The book covers such issues as quantification, equality (including a treatment of Frege's morning star/evening star puzzle), the notion of existence, non-rigid constants and function symbols, predicate abstraction, the distinction between nonexistence and nondesignation, and definite descriptions, borrowing from both Fregean and Russellian paradigms.

In 2004 the United Nations was conmemorating the tenth anniversary of the International Year of the Family. On this occasion, it was fitting to consider an aspect of education which can be developed in the family, but hardly receives much attention in that context. We refer to aesthetic education. The scope of this education is diverse: family life style, personal hygiene, manner of dressing, care in the use of material things, decorum. The latter includes the gestures and manner of speaking (...) as one interacts with others.Aesthetic education involves the proper cultivation of the external senses – touch, smell, taste, hearing and sight – and the internal senses such as the imagination, memory and life experience. The achievements in aesthetic education redound to the other spheres of education: emotional, moral, intellectual and social.By way of an example, the use of movies as a means to promote aesthetic education in the family is explained. To draw out the maximum educational potential of this medium, the active involvement of parents especially during the child’s early developmental stage is indispensable.The paper is divided into three parts: 1. The role of aesthetic education in the development of the human personality. 2. The family as the setting for aesthetic education. 3. Movies as a medium for aesthetic education. (shrink)

Susan Mills and John Beatty's propensity interpretation of fitness encountered very different philosophical criticisms by Alexander Rosenberg and Kenneth Waters. These criticisms and the rejoinders to them are both predictable and important. They are predictable as raisingkinds of issues typically associated with disposition concepts (this is established through a systematic review of the problems generated by Carnap's dispositional interpretation of all scientific terms). They are important as referring the resolution of these issues to the development of evolutionary biology. This historical (...) approach to the propensity interpretation of fitness draws attention to the precarious relation between philosophical clarification of scientific concepts and any given state of the empirical arts. (shrink)

BackgroundThe UN Convention on the Rights of Persons with Disabilities, and the reformed guardianship law in Germany, require that persons with a disability, including people with dementia in Alzheimer’s disease (PwAD), are supported in making self-determined decisions. This support is achieved through communication. While content-related communication is a deficit of PwAD, relational aspects of communication are a resource. Research in supported decision-making (SDM) has investigated the effectiveness of different content-related support strategies for PwAD but has only succeeded in improving understanding, (...) which, although one criterion of capacity to consent, is not sufficient to ensure overall capacity to consent. The aim of the ‘spatial intervention study’ of the DECIDE project is to examine an innovative resource-oriented SDM approach that focuses on relational aspects. We hypothesise that talking to PwAD in their familiar home setting (as opposed to a clinical setting) will reduce the complexity of the decision-making process and enhance overall capacity to consent. MethodsPeople with a suspected or confirmed diagnosis of dementia in Alzheimer’s disease will be recruited from two memory clinics (N = 80). We will use a randomised crossover design to investigate the intervention effect of the decision-making place on capacity to consent. Besides reasoning capacity, which is part of overall capacity to consent and will be the primary outcome, various secondary outcomes (e.g., other aspects of capacity to consent, subjective task complexity, decisional conflict) and suspected moderating or mediating variables (e.g., meaning of home, demographic characteristics) will be assessed.DiscussionThe results of the study will be used to develop a new SDM strategy that is based on relational resources for PwAD. If a change in location achieves the anticipated improvement in capacity to consent, future research should focus on implementing this SDM strategy in a cost-effective manner in clinical practice.Trial registration: DRKS00030799. (shrink)

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 (...) a natural semantics for distributed logic programs, including those involving confidence factors. The classical two-valued and the Kripke/Kleene three-valued semantics become special cases, since the logics involved are natural sublogics of Belnap’s logic, the logic given by the simplest bilattice. (shrink)

A new semantics is presented for the logic of proofs (LP), [1, 2], based on the intuition that it is a logic of explicit knowledge. This semantics is used to give new proofs of several basic results concerning LP. In particular, the realization of S4 into LP is established in a way that carefully examines and explicates the role of the + operator. Finally connections are made with the conventional approach, via soundness and completeness results.

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.

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.

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.

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 (...) language, and on what sentences will they agree? This problem can be reformulated as one about many-valued Kripke models, allowing many-valued accessibility relations. This is a natural generalization of conventional Kripke models that has only recently been looked at. The equivalence between the many-valued version and the multiple expert one will be formally established. Finally we will axiomatize many-valued modal logics, and sketch a proof of completeness. (shrink)

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.

One approach to the paradoxes of self-referential languages is to allow some sentences to lack a truth value (or to have more than one). Then assigning truth values where possible becomes a fixpoint construction and, following Kripke, this is usually carried out over a partially ordered family of three-valued truth-value assignments. Some years ago Matt Ginsberg introduced the notion of bilattice, with applications to artificial intelligence in mind. Bilattices generalize the structure Kripke used in a very natural way, while making (...) the mathematical machinery simpler and more perspicuous. In addition, work such as that of Yablo fits naturally into the bilattice setting. What I do here is present the general background of bilattices, discuss why they are natural, and show how fixpoint approaches to truth in languages that allow self-reference can be applied. This is not new work, but rather is a summary of research I have done over many years. (shrink)

In a forthcoming paper, Walter Carnielli and Abilio Rodrigues propose a Basic Logic of Evidence whose natural deduction rules are thought of as preserving evidence instead of truth. BLE turns out to be equivalent to Nelson’s paraconsistent logic N4, resulting from adding strong negation to Intuitionistic logic without Intuitionistic negation. The Carnielli/Rodrigues understanding of evidence is informal. Here we provide a formal alternative, using justification logic. First we introduce a modal logic, KX4, in which \ can be read as asserting (...) there is implicit evidence for X, where we understand evidence to permit contradictions. We show BLE embeds into KX4 in the same way that Intuitionistic logic embeds into S4. Then we formulate a new justification logic, JX4, in which the implicit evidence motivating KX4 is made explicit. KX4 embeds into JX4 via a realization theorem. Thus BLE has both implicit and explicit possibly contradictory evidence interpretations in a formal sense. (shrink)

Strict/tolerant logic, ST, evaluates the premises and the consequences of its consequence relation differently, with the premises held to stricter standards while consequences are treated more tolerantly. More specifically, ST is a three-valued logic with left sides of sequents understood as if in Kleene’s Strong Three Valued Logic, and right sides as if in Priest’s Logic of Paradox. Surprisingly, this hybrid validates the same sequents that classical logic does. A version of this result has been extended to meta, metameta, … (...) consequence levels in Barrio et al.. In my earlier paper Fitting I showed that the original ideas behind ST are, in fact, much more general than first appeared, and an infinite family of many valued logics have Strict/Tolerant counterparts. This family includes both Kleene’s and Priest’s logic individually, as well as first degree entailment. For instance, for both the Kleene and the Priest logic, the corresponding strict/tolerant logic is six-valued, but with differing sets of strictly and tolerantly designated truth values. The present paper extends that generalization in two directions. We examine a reverse notion, of Tolerant/Strict logics, which exist for the same structures that were investigated in Fitting. And we show that the generalization extends through the meta, metameta, … consequence levels for the same infinite family of many valued logics. Finally we close with remarks on the status of cut and related rules, which can actually be rather nuanced. Throughout, the aim is not the philosophical applications of the Strict/Tolerant idea, but the determination of how general a phenomenon it is. (shrink)

Strict/tolerant logic is a formally defined logic that has the same consequence relation as classical logic, though it differs from classical logic at the metaconsequence level. Specifically, it does not satisfy a cut rule. It has been proposed for use in work on theories of truth because it avoids some objectionable features arising from the use of classical logic. Here we are not interested in applications, but in the formal details themselves. We show that a wide range of logics have (...) strict/tolerant counterparts, with the same consequence relations but differing at the metaconsequence level. Among these logics are Kleene’s K3\documentclass[12pt]{minimal} \usepackage{amsmath} \usepackage{wasysym} \usepackage{amsfonts} \usepackage{amssymb} \usepackage{amsbsy} \usepackage{mathrsfs} \usepackage{upgreek} \setlength{\oddsidemargin}{-69pt} \begin{document}$$\mathsf {K_3}$$\end{document}, Priest’s LP\documentclass[12pt]{minimal} \usepackage{amsmath} \usepackage{wasysym} \usepackage{amsfonts} \usepackage{amssymb} \usepackage{amsbsy} \usepackage{mathrsfs} \usepackage{upgreek} \setlength{\oddsidemargin}{-69pt} \begin{document}$${\mathsf {LP}}$$\end{document}, and first-degree entailment, FDE. The primary tool we use is the bilattice. But it is more than a tool, it seems to be the natural home for this kind of investigation. (shrink)

While Kripke's original paper on the theory of truth used a three-valued logic, we believe a four-valued version is more natural. Its use allows for possible inconsistencies in information about the world, yet contains Kripke's development within it. Moreover, using a four-valued logic makes it possible to work with complete lattices rather than complete semi-lattices, and thus the mathematics is somewhat simplified. But more strikingly, the four-valued version has a wide, natural generalization to the family of interlaced bilattices. Thus, with (...) little more work, the theory is extended to a broad class of settings. Indeed, a result like Theorem 6.2 would not even be possible to state without the interlaced bilattice machinery. We hope the notion of interlaced bilattice will make apparent further such connections. (shrink)

This paper continues my work of [9], which showed there was a broad family of many valued logics that have a strict/tolerant counterpart. Here we consider a generalization of weak Kleene three valued logic, instead of the strong version that was background for that earlier work. We explain the intuition behind that generalization, then determine a subclass of strict/tolerant structures in which a generalization of weak Kleene logic produces the same results that the strong Kleene generalization did. This paper provides (...) much background, but is not self-contained. Some results from [9] are called on, and are not reproved here. [9] Melvin C. Fitting. “A Family of Strict/Tolerant Logics”. In: Journal of Philosophical Logic. Online. Print publication forthcoming. (shrink)

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 (...) of each other, roughly in the same way that tableaus and Gentzen sequent calculi are notational variants. This immediately gives rise to new modal nested sequent systems which may be of independent interest. We discuss some of these, including those for some justification logics that include standard modal operators. (shrink)

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 (...) between communities. In this paper we summarize one variety of approaches to the semantics of logic programs: that based on fixpoint theory. We do not attempt to cover much beyond this single area, which is already remarkably fruitful. We hope readers will see parallels with, and the divergences from the better known fixpoint treatments developed for other programming methodologies. (shrink)

First - order modal logic is very much under current development, with many different semantics proposed. The use of rigid objects goes back to Saul Kripke. More recently, several semantics based on counterparts have been examined, in a development that goes back to David Lewis. There is yet another line of research, using intensional objects, that traces back to Richard Montague. I have been involved with this line of development for some time. In the present paper, I briefly sketch several (...) of the approaches to first - order modal logic. Then I present one that I call FOIL in the Montague tradition that, I believe, is both expressive and natural. I briefly discuss in what sense it can be made to encompass the other approaches. Finally, I provide tableau rules to go with the FOIL semantics. (shrink)

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.

In the tech report Artemov and Yavorskaya [4] an elegant formulation of the first-order logic of proofs was given, FOLP. This logic plays a fundamental role in providing an arithmetic semantics for first-order intuitionistic logic, as was shown. In particular, the tech report proved an arithmetic completeness theorem, and a realization theorem for FOLP. In this paper we provide a possible-world semantics for FOLP, based on the propositional semantics of Fitting [5]. We also give an Mkrtychev semantics. Motivation and intuition (...) for FOLP can be found in Artemov and Yavorskaya [4], and are not fully discussed here.This paper is dedicated to Sergei Artemov, an honored colleague and friend, who has made wonderful things for the rest of us to play with. (shrink)

A propositional logic of explicit proofs, LP, was introduced in [S. Artemov, Explicit provability and constructive semantics, The Bulletin for Symbolic Logic 7 1–36], completing a project begun long ago by Gödel, [K. Gödel, Vortrag bei Zilsel, translated as Lecture at Zilsel’s in: S. Feferman , Kurt Gödel Collected Works III, 1938, pp. 62–113]. In fact, LP can be looked at in a more general way, as a logic of explicit evidence, and there have been several papers along these lines. (...) A major result about LP is the Realization Theorem, that says any theorem of S4 can be converted into a theorem of LP by some replacement of necessitation symbols with explicit proof terms. Thus the necessitation operator of S4 can be seen as a kind of implicit existential quantifier: there exists a proof term such that…. In this paper, quantification over evidence is introduced into LP, and it is shown that the connection between S4 necessitation and the existential quantifier becomes an explicit one. The extension of LP with quantifiers is called QLP. A semantics and an axiom system for QLP are given, soundness and completeness are established, and several results are proved relating QLP to LP and to S4. (shrink)

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 (...) natural way long-standing problems of logical omniscience. Since then, LP has become one member of a family of related logics, all logics of knowledge with explicit knowledge terms. In this paper the original problem of intuitionistic foundations is discussed only briefly. We concentrate entirely on issues of reasoning about knowledge. (shrink)

We continue a series of papers on a family of many-valued modal logics, a family whose Kripke semantics involves many-valued accessibility relations. Earlier papers in the series presented a motivation in terms of a multiple-expert semantics. They also proved completeness of sequent calculus formulations for the logics, formulations using a cut rule in an essential way. In this paper a novel cut-free tableau formulation is presented, and its completeness is proved.

Many powerful logics exist today for reasoning about multi-agent systems, but in most of these it is hard to reason about an infinite or indeterminate number of agents. Also the naming schemes used in the logics often lack expressiveness to name agents in an intuitive way.To obtain a more expressive language for multi-agent reasoning and a better naming scheme for agents, we introduce a family of logics called term-modal logics. A main feature of our logics is the use of modal (...) operators indexed by the terms of the logics. Thus, one can quantify over variables occurring in modal operators. In term-modal logics agents can be represented by terms, and knowledge of agents is expressed with formulas within the scope of modal operators. (shrink)

LP can be seen as a logic of knowledge with justifications. See [S. Artemov, The logic of justification, The Review of Symbolic Logic 1 477–513] for a recent comprehensive survey of justification logics generally. Artemov’s Realization Theorem says justifications can be extracted from validities in the more conventional Hintikka-style logic of knowledge S4, in which they are not explicitly present. Justifications, however, are far from unique. There are many ways of realizing each theorem of S4 in the logic LP. If (...) the machinery of justifications is to be applied to artificial intelligence, or better yet, to everyday reasoning, we will need to work with whatever justifications we may have at hand—one version may not be interchangeable with another, even though they realize the same S4 formula. In this paper we begin the process of providing tools for reasoning about justifications directly. The tools are somewhat complex, but in retrospect this should not be surprising. Among other things, we provide machinery for combining two realizations of the same formula, and for replacing subformulas by equivalent subformulas. The results are algorithmic in nature—semantics for LP plays no role. We apply our results to provide a new algorithmic proof of Artemov’s Realization Theorem itself. This paper is a much extended version of [M.C. Fitting, Realizations and LP, in: S. Artemov, A. Nerode , Logical Foundations of Computer Science—New York ’07, in: Lecture Notes in Computer Science, vol. 4514, Springer-Verlag, 2007, pp. 212–223]. (shrink)

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 (...) can give reasonable answers to queries that involve both negation and free variables. Also it gives the same results as Prolog when there are no negations. Finally, an implementation in Prolog is given. (shrink)

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.