Skip to main content
Fachgebiete
Automobil + Motoren Bauwesen + Immobilien Business IT + Informatik Elektrotechnik + Elektronik Energie + Nachhaltigkeit Finance + Banking Management + Führung Marketing + Vertrieb Maschinenbau + Werkstoffe Versicherung + Risiko
DE
EN
Bücher
Zeitschriften
Themenseiten
Organisationspsychologie Projektmanagement Marketing Smart Manufacturing
Weitere Formate
Podcasts Webinare Technik Webinare Wirtschaft Kongresse Veranstaltungskalender Awards
Jetzt Einzelzugang starten
Zugang für Unternehmen
Referenzkunden
SLX-Digitalkonferenz: Zukunftswerkstatt 2024

Mehr Umsatz mit Top-Kontakten

Am 7. Mai erfahren Sie, wie Vertriebsteams Leadgenerierung, Leadnurturing und Leadstrategien effizient steuern können.
Erweiterte Suche
Anmelden
nach oben

1996 | Buch

An Overview of Fibred Semantics and the Combination of Logics Kapitel lesen Erstes Kapitel lesen

Frontiers of Combining Systems

First International Workshop, Munich, March 1996

herausgegeben von: Frans Baader, Klaus U. Schulz

Verlag: Springer Netherlands

Buchreihe : Applied Logic Series

Enthalten in: Professional Book Archive

Einloggen, um Zugang zu erhalten
insite
SUCHEN

Über dieses Buch

- Donation refusal is high in all the regions of Argentina. - The deficient operative structure is a negative reality that allows inadequate donor maintenance and organ procurement. - In more developed regions, there are a high number of organs which are not utilized. This is true for heart, liver and lungs. Small waiting lists for these organs probably reflect an inadequate economic coverage for these organ transplant activities. - There is a long waiting list for cadaveric kidney transplants, which reflect poor procurement and transplant activity. - Lack of awareness by many physicians leads to the denouncing of brain deaths. In spite of these factors, we can say that there has been a significant growth in organ procuration and transplantation in 1993, after the regionalization of the INCUCAI. Conclusions Is there a shortage of organs in Argentina? There may be. But the situation in Argentina differs from that in Europe, as we have a pool of organs which are not utilized (donation refusal, operational deficits, lack of denouncing of brain deaths). Perhaps, in the future, when we are able to make good use of all the organs submitted for transplantation, we will be able to say objectively whether the number of organs is sufficient or not. Acknowledgements I would like to thank the University of Lyon and the Merieux Foundation, especially Professors Traeger, Touraine and Dr. Dupuy for the honour of being invited to talk about the issue of organ procurement.

Inhaltsverzeichnis

Frontmatter
An Overview of Fibred Semantics and the Combination of Logics
Abstract
This paper presents an overview of the authors methodology of Fibred Semantics and The Combinations of Logics presented in a series of papers under the same title. We explain the ideas behind fibring and illustrate them in several case studies. We include fibring modal and intuitionistic logics, fibring with fuzzy logics as well as self fibring of predicate logics.
Dov M. Gabbay
Generalising Propositional Modal Logic Using Labelled Deductive Systems
Abstract
A family of labelled deductive systems called Propositional Modal Labelled Deductive (PMLD) systems is described. These logics combine the standard syntax of propositional modal logic with a simple subset of first-order predicate logic, called a labelling algebra, to allow syntactic reference to a Kripke-like structure of possible worlds. PMLD systems are a generalisation of normal propositional modal logic in that they facilitate reasoning about what is true at different points in a (possibly singleton) structure of actual worlds, called a configuration. A model-theoretic semantics (based on first-order logic) is provided and its equivalence to Kripke semantics for normal propositional modal logics is shown whenever the initial configuration is a single point. A sound and complete natural deduction style proof system is also described. Unlike traditional proof systems for modal logics, this system is uniform in that every deduction rule is applicable to (the generalisation of) each normal modal logic extension of K obtained by adding combinations of the axiom schemas T, 4,5, D and B
Alessandra Russo
A Topography of Labelled Modal Logics
Abstract
Labelled Deductive Systems provide a general method for representing logics in a modular and transparent way. A Labelled Deductive System consists of two parts, a base logic and a labelling algebra, which interact through a fixed interface. The labelling algebra can be viewed as an independent parameter: the base logic stays fixed for a given class of related logics from which we can generate the one we want by plugging in the appropriate algebra. Our work identifies an important property of the structured presentation of logics, their combination, and extension. Namely, there is tension between modularity and extensibility: a narrow interface between the base logic and labelling algebra can limit the degree to which we can make use of extensions to the labelling algebra. We illustrate this in the case of modal logics and apply simple results from proof theory to give examples.
David Basin, Seán Matthews, Luca Viganò
Combining Classical and Intuitionistic Logic
Or: Intuitionistic Implication as a Conditional
Abstract
We study how a logic C+J conbining classical logic C and intuitionistic logic J can be defined. We show that its Hilbert axiomatization cannot be attained by simply extending the union of the axiomatizations of C and J by so called interaction axioms. Such a logic would collapse into classical logic.
Luis Fariñas del Cerro, Andreas Herzig
A New Correctness Proof of the Nelson-Oppen Combination Procedure
Abstract
The Nelson-Oppen combination procedure, which combines satisfiability procedures for a class of first-order theories by propagation of equalities between variables, is one of the most general combination methods in the field of theory combination. We describe a new non- deterministic version of the procedure that has been used to extend the Constraint Logic Programming Scheme to unions of constraint theories. The correctness proof of the procedure that we give in this paper not only constitutes a novel and easier proof of Nelson and Oppen’s original results, but also shows that equality sharing between the satisfiability procedures of the component theories, the main idea of the method, can be confined to a restricted set of variables.
While working on the new correctness proof, we also found a new characterization of the consistency of the union of first-order theories. We discuss and give a proof of such characterization as well.
Cesare Tinelli, Mehdi Harandi
Cooperation of Decision Procedures for the Satisfiability Problem
Abstract
Constraint programming is strongly based on the use of solvers which are able to check satisfiability of constraints. We show in this paper a rule-based algorithm for solving in a modular way the satisfiability problem w.r.t. a class of theories Th. The case where Th is the union of two disjoint theories Th 1 and Th 2 is known for a long time but we study here different cases where function symbols are shared by Th 1 and Th 2. The chosen approach leads to a highly non-deterministic decomposition algorithm but drastically simplifies the understanding of the combination problem. The obtained decomposition algorithm is illustrated by the combination of non-disjoint equational theories.
Christophe Ringeissen
Combining Finite Model Generation with Theorem Proving
Problems And Prospects
Abstract
This paper is about automatic searching for proofs, automatic searching for models and the potentially fruitful ways in which these traditionally separate aspects of reasoning may be made to interact. It takes its starting point in research reported in 1993 (Slaney, SCOTT: A Semantically Guided Theorem Prover, Proc. 13th IJCAI) on a system which combines a high performance first order theorem prover with a program generating small models of first order theories. The main theorem is an incompleteness result for a certain range of problems to which this combined system has been successfully applied. While the result may not be unexpected, the proof is worth examining and it is important to reflect on its relationship to the research program in combining methods.
John Slaney, Timothy Surendonk
Reasoning Theories
Towards an Architecture for Open Mechanized Reasoning Systems
Abstract
Our ultimate goal is to provide a framework and a methodology which will allow users, and not only system developers, to construct complex systems by composing existing modules, or to add new modules to existing systems, in a “plug and play” manner. These modules and systems might be based on different logics; have different domain models; use different vocabularies and data structures; use different reasoning strategies; and have different interaction capabilities. This paper, which is a first small step towards our goal, makes two main contributions. First, it proposes a general architecture for a class of reasoning modules and systems called Open Mechanized Reasoning Systems (OMRSs). An OMRS has three components: a reasoning theory component which is the counterpart of the logical notion of formal system, a control component which consists of a set of inference strategies, and an interaction component which provides an OMRS with the capability of interacting with other systems, including OMRSs and human users. Second, it develops the theory underlying the reasoning theory component. This development is illustrated by an analysis of the Boyer-Moore system, NQTHM.
Fausto Giunchiglia, Paolo Pecchiari, Carolyn Talcott
Natural Language Presentation and Combination of Automatically Generated Proofs
Abstract
The paper describes a generic tool that generates automatically natural language presentations of proofs from various automated and interactive deductive systems. Proofs from different sources are translated into a unified format and equipped with a block structure. These proofs can be easily combined. Several proof transformation procedures, based only on the analysis of structural aspects of the proofs, are available. The tool is part of the ILF system and of the ILF mail server.
Bernd Ingo Dahn, Andreas Wolf
Symbolic Computation: Computer Algebra and Logic
Abstract
In this paper we present our personal view of what should be the next step in the development of symbolic computation systems. The main point is that future systems should integrate the power of algebra and logic. We identify four gaps between the future ideal and the systems available at present: the logic, the syntax, the mathematics, and the prover gap, respectively. We discuss higher order logic without extensionality and with set theory as a subtheory as a logic frame for future systems and we propose to start from existing computer algebra systems and proceed by adding new facilities for closing the syntax, mathematics, and the prover gaps. Mathematica seems to be a particularly suitable candidate for such an approach. As the main technique for structuring mathematical knowledge, mathematical methods (including algorithms), and also mathematical proofs, we underline the practical importance of functors and show how they can be naturally embedded into Mathematica.
Bruno Buchberger
Classification of Communication and Cooperation Mechanisms for Logical and Symbolic Computation Systems
Abstract
The combination of logical and symbolic computation systems has recently emerged from prototype extensions of stand-alone systems to the study of environments allowing interaction among several systems. Communication and cooperation mechanisms of systems performing any kind of mathematical service enable one to study and solve new classes of problems and to perform efficient computation by distributed specialized packages. The classification of communication and cooperation methods for logical and symbolic computation systems given in this paper provides and surveys different methodologies for combining mathematical services and their characteristics, capabilities, requirements, and differences. The methods are illustrated by recent well-known examples. We separate the classification into communication and cooperation methods. The former includes all aspects of the physical connection, the flow of mathematical information, the communication language(s) and its encoding, encryption, and knowledge sharing. The latter concerns the semantic aspects of architectures for cooperative problem solving
Jacques Calmet, Karsten Homann
Logic Tuple Spaces for the Coordination of Heterogenous Agents
Abstract
This work presents ACLT, a coordination model aimed to combine and coordinate heterogeneous agents by means of a communication abstraction inspired to the Linda model, but rooted in a logic framework. The twofold interpretation of a logic tuple space both as a message and as a knowledge repository naturally induces a categorization of agents as logic and non-logic. While non-logic agents adopt the basic Linda kernel, logic agents exploit the full power of the ACLT model, which supports deduction and reasoning over the content of the tuple space. By providing a conceptual framework where logic inference and temporal tuple space evolution coexist, ACLT provides a suitable environment to build heterogeneous multi-agent systems, where hybrid agent architectures can be designed, integrating reasoning capabilities together with reactive behaviours.
Enrico Denti, Antonio Natali, Andrea Omicini, Marco Venuti
Integration Systems and Interaction Spaces
Abstract
Integration systems are abstract methods of combining theories, computational paradigms, algorithms, and other rule-driven symbolic processing systems. This paper discusses our hopes and our progress in creating a principled approach to a theory of integration for large systems. First, we discuss two types of integration systems, distinguished by the flexibility of the integration process and the types of infrastructure that they retain. In the next section of the paper, we present our approach to creating an integration infrastructure through the processing of explicit meta-knowledge. In the following section, we introduce some work on combining wrappings with text-based Virtual Reality environments to form a new kind of integration infrastructure, and in the last section, we discuss the requirements for formalisms that have emerged from working in these testbeds. This research was supported in part by the Aerospace Corporation’s Sponsored Research Program, by the Federal Highway Administration’s Office of Advanced Research, and by the Advanced Research Projects Agency’s Software and Intelligent Systems Technology Office.
Christopher Landauer, Kirstie L. Bellman
Combining Solvers in a Meta Constraint Logic Programming Architecture
Abstract
We present a general technique for the combination and the integration of different Constraint Logic Programming (CLP) solvers. The main idea behind the work concerns the possibility of building meta CLP architectures by adding CLP solvers in a natural and effective manner. In the meta architecture, levels are constraint solvers each reasoning on constraints of the underlying system. The architecture presented starts from a meta Constraint Logic Programming general scheme. A distinguishing feature of the architectural scheme concerns its operational semantics which can be seen as a general combination method for data and control of two constraint solvers. A set of linking rules define how systems exchange data, while a set of transition rules define how systems combine their control flow. We propose a specialization of a meta CLP architecture on finite domains. The specialization concerns the possibility of combining qualitative and quantitative reasoning in a CLP framework. This combination can be useful, for example, in the field of temporal reasoning.
Evelina Lamma, Michela Milano, Paola Mello
Membership-Constraints and Complexity in Logic Programming with Sets
Abstract
General agreement exists about the usefulness of sets as very high- level representations of complex data structures. Therefore it is worthwhile to introduce sets into constraint logic programming or set constraints into programming languages in general.
We start with a brief overview on different notions of sets. This seems to be necessary since there are almost as many different notions in the field as there are applications such as e.g. rapid software prototyping and unification-based grammar formalisms.
An efficient algorithm for treating membership-constraints is introduced. It is used in the implementation of an algorithm for unifying finite sets with tails also presented here. Such a unification algorithm is useful in any logic programming language embedding sets.
Finally it is shown how a full set language including the operators ∈ ∉ ∩, ∪ can be built on membership-constraints. The text closes with a reflection on the complexities of different algorithms - which are single exponential - showing the efficiency of our new algorithm
Frieder Stolzenburg
Integrating Lists, Multisets, and Sets in a Logic Programming Framework
Abstract
The first order theories of lists, bags, compact-lists (i.e., lists where the number of contiguous occurrences of each element is immaterial), and sets are introduced via axioms. Such axiomatizations are shown to be especially suitable for the integration with free functor symbols governed by the classical Clark’s axioms in the context of Constraint Logic Programming. Adaptations of the extensionality principle to the various theories taken into account is then exploited in the design of unification algorithms for the considered data structures. All the theories presented can be combined providing frameworks to deal with several of the proposed data structures simoultaneously. The unification algorithms proposed can be combined (merged) as well to produce engines for such combination theories.
Agostino Dovier, Alberto Policriti, Gianfranco Rossi
CLP(x) for Proving Program Properties
Abstract
Various proof methods have been proposed to solve the implication problem, i.e. proving that properties of the form: ∀(P → Q) - where P and Q denote conjunctions of atoms - are logical consequences of logic programs. Nonetheless, it is a commonplace to say that it is still quite a difficult problem. Besides, the advent of the constraint logic programming scheme constitutes not only a major step towards the achievement of efficient declarative logic programming systems but also a new field to explore. By recasting and simplifying the implication problem in the constraint logic programming framework, we define a generic proof method for the implication problem, which we prove sound from the algebraic point of view. We present four examples using CLP(ℕ), CLP(RT), CLP(Σ*) and RISC- CLP(RɛAℒ). The logical point of view of the constraint logic programming scheme enables the automation of the proof method. At last, we prove the unsolvability of the implication problem, we point out the origins of the incompleteness of the proposed proof method and we identify two classes of programs for which we give a decision procedure for the implication problem.
Fred Mesnard, Sébastien Horau, Alexandra Maillard
First-Order Constrained Lambda Calculus
Abstract
In (Crossley et al., 1993a; Crossley et al., 1993b; Mandel, 1995) a calculus which extends the traditional lambda calculus by the addition of constraints was presented. The constraints can be used passively for restricting the range of variables and actively for computing solutions of goals. Here we present an extension of that calculus obtained by adding existential quantifiers and new rules for handling the new terms. This avoids the problem of shared variables problem and gives a very smoothly working language. We present a proof of the Church Rosser property and the denotational semantics of the whole calculus.
John N. Crossley, Luis Mandel, Martin Wirsing
Unified Relational Framework for Programming Paradigm Combination
Abstract
The goal of this work is to provide a clean formal framework to support a development methodology for programs integrating modules of different paradigms (e.g., Horn clauses modules, equational modules, functional modules, constraints based modules, …) Modules can be developed each in its own paradigm, the framework presents a uniform and high-level view allowing to make reasoning about those modules, to build them using a uniform methodology and to combine them adequately in a realistic program.
Naji Habra, Baudouin le Charlier
Model Checking ACTL Constrained Processes
Abstract
Logical constrained processes are loose specifications for partially defined systems: they are a combination of open terms in process algebras and a constraint constructed on temporal logics. Using open terms for loose specifications provides a way to bring advantages from process algebras, yet we are not restricted to a single equivalence class due to the appearances of free variables. Furthermore, these variables are constrained by logical formulae expressing the properties they should give respect to in further refinements. In this paper, we discuss the specifications and verifications of logical constrained processes using (i) regular process (sequential and non-deterministic process) as open terms and (ii) ACTL, an action-based version of CTL, as the underlying logic for constraints. The problem of verifying a (global) property in such logical constrained process is shown to be reducible into the classical validity /satisfiability verification of ACTL formulae. The transformation follows the style of the algorithm for CTL model checking.
Xiao Jun Chen
Metadaten
Titel
Frontiers of Combining Systems
herausgegeben von
Frans Baader
Klaus U. Schulz
Copyright-Jahr
1996
Verlag
Springer Netherlands
Electronic ISBN
978-94-009-0349-4
Print ISBN
978-94-010-6643-3
DOI
https://doi.org/10.1007/978-94-009-0349-4