Terminological Logics with Modal Operators
- Franz Baader; Armin Laux
Terminological knowledge representation formalisms can be used to represent objective, time-independent facts about an application domain. Notions like belief, intentions, time---which are essential for the representation of multi-agent environments---can only be expressed in a very limited way. For such notions, modal logics with possible worlds semantics provides a formally well-founded and well-investigated basis. This paper presents a framework for integrating modal operators into terminological knowledge representation languages. These operators can be used both inside of concept expressions and in front of terminological and assertional axioms. The main restrictions are that all modal operators are interpreted in the basic logic K,...
Conquest: CONcurrent QUEries over Space and Time
- Silvia Nittel; Kenneth W. Ng; Richard R. Muntz
. The need and opportunity to efficiently find patterns and features in the vast and growing scientific data sets of today is apparent. In this paper, we present an extensible and distributed query processing system --- Conquest (CONcurrent QUEries over Space and Time) which delivers high performance for non-traditional database query applications. Conquest is composed of components: query management subsystem, query execution engine and user-interface subsystem. Both operation and data parallelism are supported. Scientists can arbitrarily introduce their familiar well-known raster and vector geometry data types as well as particular algorithms for specific applications. Tools are available to help support...
Partial Deduction System
- Michael Leuschel
We present the fully automatic partial deduction system ecce, which can be used to specialise and optimise logic programs. We describe the underlying principles of ecce and illustrate some of the potential application areas. Interesting possibilites of crossfertilisation with other fields such as reachability analysis of concurrent systems and inductive theorem proving are highlighted and substantiated. 1 Introduction Program specialisation, also called partial evaluation or partial deduction, is an automatic technique for program optimisation. The central idea is to specialise a given source program for a particular application domain. Program specialisation encompasses traditional compiler optimisation techniques, such as constant folding...
Specification and Prototyping of Network Protocols in Rewriting Logic
- Peter Csaba Olveczky; Peter Csaba; Sigurd Meldal
this article is the latter. 1.1 Executable specifications
A Proof Presentation Suitable for Teaching Proofs
- Erica Melis; Fachbereich Informatik; Uri Leron
. The paper addresses comprehensible proof presentation for teaching and learning that can be provided by an automated proof planner that is a component of the proof development environment\Omega mega. Starting from empirically discovered requirements for the comprehensibility of proofs we show that, given a proof plan representation of a proof, the problem of automatically presenting a mathematical proof in a comprehensible manner becomes feasible in a way that was impossible before. We show how, based on a proof plan, a structured presentation at the level of proof methods can be automatically constructed 1 Introduction Computer algebra systems have been...
A Uniform Framework for Concept Definitions in Description Logics
- Giuseppe De Giacomo; Maurizio Lenzerini
Most modern formalisms used in Databases and Artificial Intelligence for describing an application domain are based on the notions of class (or concept) and relationship among classes. One interesting feature of such formalisms is the possibility of defining a class, i.e., providing a set of properties that precisely characterize the instances of the class. Many recent articles point out that there are several ways of assigning a meaning to a class definition containing some sort of recursion. In this paper, we argue that, instead of choosing a single style of semantics, we achieve better results by adopting a formalism that...
Hardware-Software Codesign of Multidimensional Programs
- Wayne Luk; Teddy Wu; Ian Page
We present a method for parametrised partitioning of multidimensional programs for acceleration using a hardware coprocessor. The method involves a divide-andconquer structure, with the "divide" and "merge" phases carried out by a general-purpose processor while the "conquer " phase is handled by application-specific hardware. The partitioning strategy has been captured in a simple functional language, and we have automated the production of partitioned programs in this language. Our approach has been tested on an FPGA-based system using a number of computer vision algorithms,including the Canny edge detector, and the performance is compared against executing the programs on the PC host....
Using Model-Checking for Timed Automata to Parameterize Logic Control Programs
- Stefan Kowalewski; Sebastian Engell; Ralf Huuck; Yassine Lakhnech; Ben Lukoschus; Luis Urbina
In this contribution we describe how the modeling and analysis framework of Timed Automata can be used to determine valid parameter ranges for timers in logic control programs. The procedure is illustrated by means of a simple process engineering example for which the complete Timed Automata model is presented. To analyse the model, the tool HyTech is used which provides routines to determine values of model parameters depending on reachability conditions. Keywords: Programmable Logic Controllers, process safety, validation, Timed Automata, HyTech. INTRODUCTION When Programmable Logic Controllers (PLCs) are used in process control, often the problem arises that the correct timing...
Transformation-Based Learning meets Frequent Pattern Discovery
- Luc Dehaspe; Maarten Forrier
Transformation-based learning (TBL) and frequent pattern discovery (FPD) are two popular research paradigms, one from the domain of empirical natural language processing, the second from the field of data mining. This paper describes how Eric Brill's original TBL algorithm can be improved via incorporation of FPD techniques. The algorithm B-Warmr is presented that upgrades TBL to first-order logic and speeds up the search for transformations, also in the original propositional case. We demonstrate some scaling properties of B-Warmr and discuss how the algorithm can be tuned to generate (first-order) decision lists. We also propose a new method, Disjunctive TransformationBased Learning...
Modularized Context-Free Grammars
- Shuly Wintner
Given two context-free grammars (CFGs), G 1 and G 2 , the language generated by the union of the grammars is not the union of the languages generated by each grammar: L(G 1 [ G 2 ) 6= L(G 1 ) [ L(G 2 ). In order to account for modularity of grammars, another way of defining the meaning of grammars is needed. This paper adapts results from the semantics of logic programming languages to CFGs. We discuss alternative approaches for defining the denotation of a grammar, culminating in one which we show to be both compositional and fullyabstract. We...
Formalising UML Use Cases in the Refinement Calculus
- Ralph-johan Back; Luigia Petre; Ivan Porres; Iv An Porres Paltor; Fin- Turku
The Unified Modeling Language (UML) consists of a set of diagrams that describe a system under development. A use case diagram specifies the required functionality of the system, showing the collaboration among a set of actors that are to perform certain tasks. We enhance use case diagrams by providing formal documents (like specifications or programs), called contracts that regulate the behaviour of the agents involved. These agents could be programs, modules, systems, users. The contract is written in a language with a precise semantics and logic for reasoning, the refinement calculus. Hence, it can be analysed for the preconditions required...
A Tailored Real Time Temporal Logic for Specifying Requirements of Building Automation Systems
- Martin Kronenburg; Reinhard Gotzhein; Christian Peper; Martin Kronenburg; Martin Kronenburg; Reinhard Gotzhein; Reinhard Gotzhein; Christian Peper; Christian Peper
A tailored real time temporal logic for specifying requirements of building automation systems is introduced and analyzed. The logic features several new real time operators, which are chosen with regard to the application area. The new operators improve the conciseness and readability of requirements as compared to a general--purpose real time temporal logic. In addition, some of the operators also enhance the expressiveness of the logic. A number of properties of the new operators are presented and proven. 1 Introduction This paper presents the formal background developed and used during a case study performed in the context of the Sonderforschungsbereich...
Some Intuitions Behind Realizability Semantics for Constructive Logic: Tableaux and Läuchli countermodels.
- James Lipton; Lauchli Countermodels; Michael J. O'donnell
We use formal semantic analysis based on new, model-theoretic constructions to generate intuitive confidence that the Heyting Calculus is an appropriate system of deduction for constructive reasoning. Well-known modal semantic formalisms have been defined by Kripke and Beth, but these have no formal concepts corresponding to constructions, and shed little intuitive light on the meanings of formulae. In particular, the well-known completeness proofs for these semantics do not generate confidence in the sufficiency of the Heyting Calculus, since we have no reason to believe that every intuitively constructive truth is valid in the formal semantics. Lauchli has proved completeness for...
A Compositional Partial Order Semantics for Petri Net Components
- Ekkart Kindler
In this paper we introduce the concept of a Petri net component and show how systems can be composed from components. A component communicates with its environment via distinguished input and output places, which formalizes communication by message passing. Then, we present a compositional semantics for components. The semantics is an extension of processes for place/transition systems (partial order semantics). We show that the semantics is fully abstract with respect to the behaviour of closed components (essentially, processes of place/transition systems). A main feature of the compositional semantics is that composition of components corresponds to conjunction. The semantics can be...
EXPTIME Tableaux for ALC (Extended Abstract)
- Guiseppe De Giacomo; Francesco M. Donini; Fabio Massacci
) Giuseppe De Giacomo 1 and Francesco M. Donini 1 and Fabio Massacci 1;2 1 Dip. Di Informatica e Sistemistica, Univ. di Roma I "La Sapienza", Italy fdegiacomo,donini,email@example.com 2 Computer Laboratory, Cambridge University, England Fabio.Massacci@cl.cam.ac.uk 1 Motivations We propose a tableaux calculus requiring simple exponential time for satisfiability of an ALC concept C wrt a TBox T containing general axioms of the form C v D. ?From correspondences with Propositional Dynamic Logic (PDL) it is known that this problem is in EXPTIME [ Pratt, 1978; Vardi and Wolper, 1986 ] . However, an algorithm directly derived from the methods used...
Estimating Logic Cell to I/O Pad Lengths in Computer Systems
- Dirk Stroobandt; Herwig Van Marck; Jan Van Campenhout
Increasing system complexity imposes high demands on computer aided design (CAD) tools for system synthesis. Especially the layout (placement and routing) of a design has become a problem hard to solve. To find a `good' layout, CAD tools need accurate estimators to predict area requirements, interconnection lengths, power dissipation, etc. In this paper we address the estimation of interconnection lengths. Previous work on this subject is primarily based on a technique introduced by Donath  which has been improved by Stroobandt et al . However, this technique only estimates interconnection lengths between two cells within the system or chip. Of...
A Type-Based Debugging Tool for Untyped Logic Languages
- Ulrich Geske; Mario Lenz
This paper presents a method for debugging type errors in untyped logic programs by generating type information based on abstract interpretation with OLDT resolution. The notion "type" is extended to enable the phenomena in logic programs to be described more precisely. The classes Single Types and Collected Types are introduced. An extended OLDT resolution performs combination of derived single types to collected types. Application of the different types for debugging unmodular and modular logic programs is discussed, and an extension of the module interface format proposed. 1 Introduction Having the opportunity to use untyped logic languages is very convenient for...
Modular Implementation of Individual Reasoning in
- Protodl The; Alex Borgida; Daniel Kudenko
This is the second report in a series on the PROTODL system, which is an *extensible* knowledge representation and reasoning system based on Description Logics (DLs). We have motivated elsewhere [Borgida&Brachman92, Borgida92] the utility of being able to add new concept constructors to a DL, and, while in previous papers we have concentrated on subsumption reasoning, in this paper we consider reasoning about individuals. We present the modular implementation of a Description Logic-based KBMS which performs inferences about individuals in such a way that the addition of each new concept constructors is achieved by introducing a series of functions (and...
Formalizing the Transformational Design of Communicating Systems in the Theorem Prover LAMBDA
- Jürgen Bohn
This paper presents the implementation of a transformational approach in the system LAMBDA, a proof checker for higher order logic. The approach aims at the design of communicating systems and is based on a sophisticated semantic model originating from the ESPRIT Basic Research Action "ProCoS" [Bjø89]. The implementation is used for the formal verification of transformation rules and for the application of proved rules to synthesize parallel systems. Unlike other approaches [BvW90] explicit names, types and values are used for program variables and channels. 1 The transformational approach We pursue a transformational approach where specifications of communicating systems are transformed...
Modular Verification of SRT Division
- Harald Rueß; Natarajan Shankar; Mandayam K. Srivas
. We describe a formal specification and mechanized verification in PVS of the general theory of SRT division along with a specific hardware realization of the algorithm. The specification demonstrates how attributes of the PVS language (in particular, predicate subtypes) allow the general theory to be developed in a readable manner that is similar to textbook presentations, while the PVS table construct allows direct specification of the implementation's quotient lookup table. Verification of the derivations in the SRT theory and for the data path and lookup table of the implementation are highly automated and performed for arbitrary, but finite precision;...