The Joint International Conference on Logic Programming, sponsored by the Association for Logic Programming, is a major forum for presentations of research, applications, and implementations in this important area of computer science. Logic programming is one of the most promising steps toward declarative programming and forms the theoretical basis of the programming language Prolog and its various extensions. Logic programming is also fundamental to work in artificial intelligence, where it has been used for nonmonotonic and commonsense reasoning, expert systems implementation, (...) deductive databases, and applications such as computer-aided manufacturing. Krzysztof R. Apt is project leader at the Centre for Mathematics and Computer Science in Amsterdam and part-time Professor in Computer Science at the University of Amsterdam. Topics covered: Theory Foundations. Programming Languages. Implementation. Programming Methodologies and Tools. Applications. Deductive Databases. Artificial Intelligence. Parallelism. (shrink)

The First International Workshop brings together researchers from the theoretical ends of the logic programming and artificial intelligence communities to discuss their mutual interests. Logic programming deals with the use of models of mathematical logic as a way of programming computers, where theoretical AI deals with abstract issues in modeling and representing human knowledge and beliefs. One common ground is nonmonotonic reasoning, a family of logics that includes room for the kinds of variations that can be found in human (...) reasoning. Topics covered: Stable Semantics. Default Logic. AutoEpistemic Logic. Truth Maintenance Systems. Implementation Issues. Diagnosis. Applications. Inheritance Reasoning. Logics of Belief. Inconsistency and Non-Monotonicity. (shrink)

Biró, B. and I. Sain, Peano arithmetic as axiomatization of the time frame in logics of programs and in dynamic logics, Annals of Pure and Applied Logic 63 201-225. We show that one can prove the partial correctness of more programs using Peano's axioms for the time frames of three-sorted time models than using only Presburger's axioms, that is it is useful to allow multiplication of time points at program verification and in dynamic and temporal (...) class='Hi'>logics. We organized the paper as follows: 1. Preliminaries, 2. The main result, 3. Peano arithmetic with bounded multiplication, 4. Connections with temporal logics and dynamic logics, Acknowledgements, References. (shrink)

A combination of epistemic logic and dynamic logic of programs is presented. Although rich enough to formalize some simple game-theoretic scenarios, its axiomatization is problematic as it leads to the paradoxical conclusion that agents are omniscient. A cut-free labelled Gentzen-style proof system is then introduced where knowledge and action, as well as their combinations, are formulated as rules of inference, rather than axioms. This provides a logical framework for reasoning about games in a modular and systematic way, and to (...) give a step-by-step reconstruction of agents omniscience. In particular, its semantic assumptions are made explicit and a possible solution can be found in weakening the properties of the knowledge operator. (shrink)

We present a logical calculus for reasoning about information flow in quantum programs. In particular we introduce a dynamic logic that is capable of dealing with quantum measurements, unitary evolutions and entanglements in compound quantum systems. We give a syntax and a relational semantics in which we abstract away from phases and probabilities. We present a sound proof system for this logic, and we show how to characterize by logical means various forms of entanglement (e.g. the Bell states) and (...) various linear operators. As an example we sketch an analysis of the teleportation protocol. (shrink)

It is shown that the infinite-valued first-order Gödel logic G° based on the set of truth values {1/k: k ε w {0}} U {0} is not r.e. The logic G° is the same as that obtained from the Kripke semantics for first-order intuitionistic logic with constant domains and where the order structure of the model is linear. From this, the unaxiomatizability of Kröger's temporal logic of programs (even of the fragment without the nexttime operator O) and of the authors' (...) temporal logic of linear discrete time with gaps follows. (shrink)

This article aims to present part of the results from the Scientific Initiation research entitled Logical Foundations of Education for Thinking. Specifically, the exposed contents are the logical ones developed by Matthew Lipman in his philosophical novel Harry Stottlemeier’s discovery. The text is divided in three main sections: formal logic, logic of good reasons and logic of rationally acting. In the first one, we map the contents of formal logic present in that novel. In this context, we studied Aristotelian logic (...) in a progressive manner, passing from the simplest elements to the more complex, namely: the categorical propositions, the reversal of categorical propositions, standardization, the table of opposites, the logic of relations and, finally, the Aristotelian syllogism . After that, we deal with other aspects of formal logic worked in Lipman’s view. They are: the hypothetical syllogism, induction, the logical relationship between part and whole, the four possibilities and tautologies. In the second section, we present an approach about the logic of good reasons. Finally, the third and final section, entitled The Logic of rationally acting, the emphasis lies in the constant and daily use of reflection, in other words, we see that the logic of rationally acting is targeting the use of reflective thinking to obtain a reasonable behavior. (shrink)

The modal logician's notion of possible world and the computer scientist's notion of state of a machine provide a point of commonality which can form the foundation of a logic of action. Extending ordinary modal logic with the calculus of binary relations leads to a very natural logic for describing the behavior of computer programs.

This volume presents a collection of refereed papers reflecting the state of the art in the area of over-constrained systems. Besides 11 revised full papers, selected from the 24 submissions to the OCS workshop held in conjunction with the First International Conference on Principles and Practice of Constraint Programming, CP '95, held in Marseilles in September 1995, the book includes three comprehensive background papers of central importance for the workshop papers and the whole field. Also included is an introduction by (...) one of the volume editors together with a bibliography listing 243 entries. All in all this is a very useful reference book relevant for all researchers and practitioners interested in hierarchical, partial, and over-constrained systems. (shrink)

An algebraic approach to programs called recursive coroutines — due to Janicki [3] — is based on the idea to consider certain complex algorithms as algebraics models of those programs. Complex algorithms are generalizations of pushdown algorithms being algebraic models of recursive procedures (see Mazurkiewicz [4]). LCA — logic of complex algorithms — was formulated in [11]. It formalizes algorithmic properties of a class of deterministic programs called here complex recursive ones or interacting stacks-programs, for which (...) complex algorithms constitute mathematical models. LCA is in a sense an extension of algorithmic logic as initiated by Salwicki [14] and of extended algorithmic logic EAL as formulated and examined by the present author in [8], [9], [10]. In LCA — similarly as in EAL-ω + -valued logic is applied as a tool to construct control systems (stacks) occurring in corresponding algorithms. The aim of this paper is to give a complete axiomatization. of LCA and to prove a completeness theorem. (shrink)

Design research programs attempt to bring together the properties of available materials and the demands derived from intended applications. The logic of problem states and state transitions in such programs, including assessment criteria and heuristic principles, is described in settheoretic terms, starting with a naive model comprising an intended profile and the operational profile of a prototype. In a first concretization the useful distinction between structural and functional properties is built into the model. In two further concretizations the (...) inclusion of potential applications is motivated and described for the case of drug research as well as the inclusion of potential realizations for the case of complex products. Next, another line of concretization of the naive model, the incorporation of potentially relevant properties, is sketched. Then the partial analogy between product- and truth-approximation is indicated. We conclude with some remarks about the usefulness of our models for products reaching the market in comparison to the the so-called social construction of technology approach. (shrink)

Originally published in 1966. This is a self-instructional course intended for first-year university students who have not had previous acquaintance with Logic. The book deals with "propositional" logic by the truth-table method, briefly introducing axiomatic procedures, and proceeds to the theory of the syllogism, the logic of one-place predicates, and elementary parts of the logic of many-place predicates. Revision material is provided covering the main parts of the course. The course represents from eight to twenty hours work. depending on the (...) student's speed of work and on whether optional chapters are taken. (shrink)

In the paper, Jan Łukasiewicz’s program of the logicization of philosophy is presented and discussed. Łukasiewicz, known mostly for his invention of trivalent logic as well as his achievements in propositional calculus and metalogic, had always been concerned with the methodological condition of philosophy. He finally found “the measure of exactness” in mathematical logic. According to him, only the use of logical tools may provide philosophical investigations with an appropriate level of exactness. He expressed his views most firmly and directly (...) in the paper, “A call for the method of Philosophy”. Łukasiewicz proposed giving philosophical theories the form of axiomatic systems by indicating the primitive terms of their language, selecting suitable axioms, and explicitly determining the applied rules of inference. All the theses of these systems should be consequences of the accepted axioms and confronted with the data of experience and the results of science. Łukasiewicz’s program is presented together with its inspirations and prospects. (shrink)

Mathematical models are an important tool in the development ofsoftware technology, including programming languages and algorithms.During the last few years, a new class of such models has beendeveloped based on the notion of a mathematical game that isespecially well-suited to address the interactions between thecomponents of a system. This paper gives an introduction to thesegame-semantical models of programming languages, concentrating onmotivating the basic intuitions and putting them into context.

We investigate synonymy in the strong sense of content identity. This notion is central in the philosophy of language and in applications of logic. We motivate, uniformly axiomatize, and characterize several “benchmark” notions of synonymy in the messy class of all possible notions of synonymy. This class is divided by two intuitive principles that are governed by a no-go result. We use the notion of a scenario to get a logic of synonymy which is the canonical representative of one division. (...) In the other division, the so-called conceptivist logics, we find, e.g., the well-known system of analytic containment. We axiomatize four logics of synonymy extending AC, relate them semantically and proof-theoretically to SF, and characterize them in terms of weak/strong subject matter preservation and weak/strong logical equivalence. This yields ways out of the no-go result and novel arguments—independent of a particular semantic framework—for each notion of synonymy discussed. This points to pluralism about meaning and a certain non-compositionality of truth in logic programs and neural networks. And it unveils an impossibility for synonymy: if it is to preserve subject matter, then either conjunction and disjunction lose an essential property or a very weak absorption law is violated. (shrink)

The purpose of this paper is to contribute to the natural logic program which invents logics in natural language. This study presents two logics: a logical system called d R containing transitive verbs and a more expressive logical system R containing both transitive verbs and intersective adjectives. The paper offers three different set-theoretic semantics which are equivalent for the logics.

The Logic of Metaphor uses techniques from possible worlds semantics to provide formal truth-conditions for many grammatical classes of metaphors. It gives logically precise and practically useful syntactic and semantic rules for generating and interpreting metaphors. These rules are implemented in a working computer program. The book treats the lexicon as a conceptual network with semantics provided by an intensional predicate calculus. It gives rules for finding analogies in such networks. It shows how to syntactically and semantically analyze texts containing (...) metaphors and how to use structural similarities between parts of possible worlds to provide truth-conditions for metaphors. Meanings for metaphors are linked to the modal logics of identity and indiscernibility. The book shows how to extend deductive and abductive inference systems to handle metaphors. It shows how to handle novel metaphorical word-senses. The Logic of Metaphor will be useful to philosophers, logicians, linguists, and computer scientists. (shrink)

Sets out the basic theory of normal modal and temporal propositional logics; applies this theory to logics of discrete (integer), dense (rational), and continuous (real) time, to the temporal logic of henceforth, next, and until, and to the propositional dynamic logic of regular programs.

Includes tutorials, invited lectures, and refereed papers on all aspects of logic programming including: Constraints, Concurrency and Parallelism, Deductive Databases, Implementations, Meta and Higher-order Programming, Theory, and Semantic Analysis. September 2-6, 1996, Bonn, Germany Every four years, the two major international scientific conferences on logic programming merge in one joint event. JICSLP'96 is the thirteenth in the two series of annual conferences sponsored by The Association for Logic Programming. It includes tutorials, invited lectures, and refereed papers on all aspects of (...) logic programming including: Constraints, Concurrency and Parallelism, Deductive Databases, Implementations, Meta and Higher-order Programming, Theory, and Semantic Analysis. The contributors are international, with strong contingents from the United States, United Kingdom, France, and Japan. Logic Programming series, Research Reports and Notes. (shrink)

Peirce algebras combine sets, relations and various operations linking the two in a unifying setting. This paper offers a modal perspective on Peirce algebras. Using modal logic a characterization of the full Peirce algebras is given, as well as a finite axiomatization of their equational theory that uses so-called unorthodox derivation rules. In addition, the expressive power of Peirce algebras is analyzed through their connection with first-order logic, and the fragment of first-order logic corresponding to Peirce algebras is described in (...) terms of bisimulations. (shrink)

In this paper, I set out some basic elements of a deontic logic with an implementation appropriate for handling conflicting legal obligations for purposes of programming autonomous machine agents. Kantian justice demands that the prescriptive system of enforceable public laws be consistent, yet statutes or case holdings may often describe legal obligations that contradict; moreover, even fundamental constitutional rights may come into conflict. I argue that a deontic logic of the law should not try to work around such conflicts but, (...) instead, identify and expose them so that the rights and duties that generate inconsistencies in public law can be explicitly qualified and the conflicts resolved. I then argue that a credulous, non-monotonic deontic logic can describe inconsistent legal obligations while meeting Kant’s demand for consistency in the prescriptive system of public law. Finally, I propose an implementation of this logic via a modified form of “answer set programming,” which I demonstrate with some simple examples. (shrink)

Another theme of the book is compilation techniques to boost performance. The field of static analysis for logic programs is a rapidly developing field that deserves a volume on its own. Implementations of Logic Programming Systems serves as an excellent reference and may be used as a text for a course on the subject.

Work on 'can' in Action Theory is dichotomized into two styles of analysis: (1) what I call the indeterministic analysis, whereby for x to be able to do A means that there is no obstacle to x's doing A, and (2) the hypothetical analysis, which asserts that x is able to do A if and only if x will do A if x tries (wants, wills, chooses, etc.). This paper explores the general hypothesis that 'can' is two-ways ambiguous, that a (...) sense of opportunity corresponds to (1) and a sense of ability to something after the pattern of (2), and that a general concept of 'can' of the kind often sought after by action theorists requires a certain kind of integration of both concepts into a unified definition. The two previous most well-worked-out attempts to lay out a program along these lines, those of Sellars and Chisholm, are analyzed in detail in the hope of smoothing out some of the technical differences to provide foundations for further work of this type. An attempt is made to integrate the program with some recent developments in the concept of ability in the social sciences. The applicability of this work to some very vexing and significant problems in the social sciences is suggested. (shrink)

In the present article we exploit the logical notions of correctness and completeness to provide an analysis of some fundamental problems that can be encountered by a software developer when transforming norms for traffic circulation into programming instructions. Relying on this analysis, we then introduce a question and answer procedure that can be helpful, in case of an accident, to clarify which components of an existing framework should be revised and to what extent software developers can be held responsible.

These two volumes collect papers presented at the first joint meeting of the two principal logic programming conferences, held in August of 1988. The more than fifty contributions cover all aspects of the field, including applications (particularly those that exploit the unique character of logic programming), the role of logic programming in artificial intelligence, deductive databases, relations to other computational paradigms, language issues, methodology, implementations on sequential and parallel architectures, and theory.Logic Programming is included in the Logic Programming series Research (...) Reports and Notes, edited by Ehud Shapiro. (shrink)

This book describes in detail the relationship between symbolic representations of knowledge and abstract states of knowledge, exploring along the way the foundations of knowledge, knowledge bases, knowledge-based systems, and knowledge representation and reasoning. The idea of knowledge bases lies at the heart of symbolic, or "traditional," artificial intelligence. A knowledge-based system decides how to act by running formal reasoning procedures over a body of explicitly represented knowledge—a knowledge base. The system is not programmed for specific tasks; rather, it is (...) told what it needs to know and expected to infer the rest. This book is about the logic of such knowledge bases. It describes in detail the relationship between symbolic representations of knowledge and abstract states of knowledge, exploring along the way the foundations of knowledge, knowledge bases, knowledge-based systems, and knowledge representation and reasoning. Assuming some familiarity with first-order predicate logic, the book offers a new mathematical model of knowledge that is general and expressive yet more workable in practice than previous models. The book presents a style of semantic argument and formal analysis that would be cumbersome or completely impractical with other approaches. It also shows how to treat a knowledge base as an abstract data type, completely specified in an abstract way by the knowledge-level operations defined over it. (shrink)

Peirce algebras combine sets, relations and various operations linking the two in a unifying setting. This paper offers a modal perspective on Peirce algebras. Using modal logic as a characterization of the full Peirce algebras is given, as well as a finite axiomatization of their equational theory that uses so-called unorthodox derivation rules. In addition, the expressive power of Peirce algebras is analyzed through their connection with first-order logic and the fragment of first-order logic corresponding to Peirce algebras is described (...) in terms of bisimulations. (shrink)

In the tradition of Denotational Semantics one usually lets program constructs take their denotations in reflexive domains, i.e. in domains where self-application is possible. For the bulk of programming constructs, however, working with reflexive domains is an unnecessary complication. In this paper we shall use the domains of ordinary classical type logic to provide the semantics of a simple programming language containing choice and recursion. We prove that the rule of {\em Scott Induction\/} holds in this new setting, prove soundness (...) of a Hoare calculus relative to our semantics, give a direct calculus ${\cal C}$ on programs, and prove that the denotation of any program $P$ in our semantics is equal to the union of the denotations of all those programs $L$ such that $P$ follows from $L$ in our calculus and $L$ does not contain recursion or choice. (shrink)

Since theism is the tradition most clearly and considerably involved in Hartshorne's program it may be useful at the outset to sketch that view.

Continuity is perhaps the most familiar characterization of the finitary character of the operations performed in computation. We sketch the historical and conceptual development of this notion by interpreting it as a unifying theme across three main varieties of semantical theories of programming: denotational, axiomatic and event-based. Our exploration spans the development of this notion from its origins in recursion theory to the forms it takes in the context of the more recent event-based analyses of sequential and concurrent computations, touching (...) upon the relations of continuity with non-determinism. (shrink)

The connection between logic programming and formal argumentation has been studied starting from the landmark 1995 paper of Dung. Subsequent work has identified a standard translation from logic programs to argumentation frameworks, under which pairwise correspondences hold between various logic programming semantics and various formal argumentation semantics. This includes the correspondence between 3-valued stable and complete semantics, between well-founded and grounded semantics and between 2-valued stable and stable semantics. In the current paper, we show that the existing translation is (...) able to yield the additional correspondence between ideal semantics for logic programming and ideal semantics for formal argumentation. We also show that correspondence does not hold between eager semantics for logic programming and eager semantics for formal argumentation, at least when translating from logic programming to formal argumentation. Overall, the current work should be seen as completing the analysis of correspondences between mainstream admissibility-based argumentation semantics and their logic programming counterparts. (shrink)

We introduce the logic LRC, designed to describe and reason about agents’ abilities and capabilities in using resources. The proposed framework bridges two—up to now—mutually independent strands of literature: the one on logics of abilities and capabilities, developed within the theory of agency, and the one on logics of resources, motivated by program semantics. The logic LRC is suitable to describe and reason about key aspects of social behaviour in organizations. We prove a number of properties enjoyed by (...) LRC and its associated analytic calculus. These results lay at the intersection of the algebraic theory of unified correspondence and the theory of multitype calculi in structural proof theory. Case studies are discussed which showcase several ways in which this framework can be extended and enriched while retaining its basic properties, so as to model an array of issues, both practically and theoretically relevant, spanning from planning problems to the logical foundations of the theory of organizations. (shrink)

Intermediary metabolism molecules are orchestrated into logical pathways stemming from history (L-amino acids, D-sugars) and dynamic constraints (hydrolysis of pyrophosphate or amide groups is the driving force of anabolism). Beside essential metabolites, numerous variants derive from programmed or accidental changes. Broken down, variants enter standard pathways, producing further variants. Macromolecule modification alters enzyme reactions specificity. Metabolism conform thermodynamic laws, precluding strict accuracy. Hence, for each regular pathway, a wealth of variants inputs and produces metabolites that are similar to but not (...) the exact replicas of core metabolites. As corollary, a shadow, paralogous metabolism, is associated to standard metabolism. We focus on a logic of paralogous metabolism based on diversion of the core metabolic mimics into pathways where they are modified to minimize their input in the core pathways where they create havoc. We propose that a significant proportion of paralogues of well-characterized enzymes have evolved as the natural way to cope with paralogous metabolites. A second type of denouement uses a process where protecting/deprotecting unwanted metabolites - conceptually similar to the procedure used in the laboratory of an organic chemist - is used to enter a completely new catabolic pathway. (shrink)

The question of the extent to which one can rationally reconstruct the process of medical diagnosis and reduce it to an algorithm is explored. The act of diagnostic insight is such that a computational program cannot ‘catch on’ in the way that a competent diagnostician can. Clinical diagnostic reasoning in a particular case requires as a necessary condition an extraordinarily complex and rich structure of background knowledge as well as an intuitive element, such as is manifest when one ‘catches on’ (...) to a joke. Computers cannot ‘catch on’ due to their limitations in the computational mode. As a consequence, there can be no computer simulation of an essential element in diagnostic procedures. Keywords: clinical judgment, computer diagnosis, intuition, medical decision-making CiteULike Connotea Del.icio.us What's this? (shrink)