381.
A survey of fuzzy logic monitoring and control utilisation in medicine
- D. A. Linkens; M. F. Abbod; M. Mahfouf
ABSTRACT: Intelligent systems have appeared in many technical areas, such as consumer electronics, robotics and industrial control systems. Many of these intelligent systems are based on fuzzy control strategies which describe complex systems mathematical model in terms of linguistic rules. Since the 1980s new techniques have appeared from which fuzzy logic been applied extensively in medical systems. This paper surveys the utilisation of fuzzy logic control and monitoring in medical sciences.
382.
LISPLOG: UMA LINGUAGEM PARA A PROGRAMAÇÃO FUNCIONAL E PARA A PROGRAMAÇÃO EM LÓGICA
- DANTE CORBUCCI FILHO
Esta dissertação apresenta uma integração entre a programação funcional e a programação em lógica, obtida pela definição e implementação da Linguagem LispLog. Nesta nova linguagem, o resultado de uma resolução pode ser utilizado como argumento de uma função (pelo operador metalisp) e o resultado da avaliação de uma função pode ser ligado a uma variável lógica (pelo operador avalia). A construção desta linguagem foi realizada a partir da simulação, em microcomputador similar ao IBM-PC, de uma máquina com arquitetura de pilhas, chamada Máquina LispLog, e de seu compilador. A utilização desta linguagem é possível através do Sistema LispLog, que fornece...
383.
A Higher Order Rewriting Logic for Functional Logic Programming
- J. Carlos Gonzalez-moreno; M. Teresa Hortala-gonzalez; Mario Rodríguez-Artalejo
According to a well known conception, programs in a declarative programming language can be viewed as theories in some suitable logic, while computations can be viewed as deductions. In our opinion, there is yet no general assent on the logic to be viewed as the foundation of higher order, lazy functional logic languages. In this paper, we argue that a specific rewriting logic can play this role, and we justify the adequacy of our proposal by means of proof-theoretical and model-theoretical results. Moreover, we present a sound and complete lazy narrowing calculus for goal solving, and we discuss a circuit...
384.
Congruence Classes with Logic
We are improving equality reasoning in automatic theorem-provers, and congruence classes provide
an e#cient storage mechanism for terms, as well as the congruence closure decision procedure. We
describe the technical steps involved in integrating logic variables with congruence classes, and present
an algorithm that can be proved to find all matches between classes (modulo certain equalities). An
application of this algorithm makes possible a percolation algorithm for undirected rewriting in
minimal space; this is described and an implementation in hol98 is examined in some detail. 1
Keywords: Congruence Closure, Equality Reasoning
1
385.
Congruence Classes with Logic
We are improving equality reasoning in automatic theorem-provers, and congruence classes provide
an ecient storage mechanism for terms, as well as the congruence closure decision procedure. We
describe the technical steps involved in integrating logic variables with congruence classes, and present
an algorithm that can be proved to
nd all matches between classes (modulo certain equalities). An
application of this algorithm makes possible a percolation algorithm for undirected rewriting in
minimal space; this is described and an implementation in hol98 is examined in some detail.
386.
On TLA as a Logic
this paper we describe TLA from a logical perspective# our
description of TLA has three aspects:
1'
As a logic, TLA has a precise syntax and semantics. We define these in
the next section. Our intent is not to develop a new TLA, but rather to
explain and to refine Lamport's definition of TLA [1'
2. Like HOL [1' ] and other logics, TLA can serve for representing reactive
systems in several styles. In particular, a specification may describe
concurrent steps as interleaved or simultaneous# communication between
components may be synchronous or asynchronous. We discuss a few styles
in section 3
387.
Higher Order Logic
- Daniel Leivant
Contents
1 Introduction : : : : : : : : : : : : : : : : : : : : : : : : : : : : 2
2 The expressive power of second order Logic : : : : : : : : : : : 3
2.1 The language of second order logic : : : : : : : : : : : : : 3
2.2 Expressing size : : : : : : : : : : : : : : : : : : : : : : : : 4
2.3 Defining data types...
388.
Higher Order Logic
- Daniel Leivant
Contents
1 Introduction : : : : : : : : : : : : : : : : : : : : : : : : : : : : 2
2 The expressive power of second order Logic : : : : : : : : : : : 3
2.1 The language of second order logic : : : : : : : : : : : : : 3
2.2 Expressing size : : : : : : : : : : : : : : : : : : : : : : : : 4
2.3 Defining data types...
389.
Synchronous Logic Synthesis:
- Giovanni De Micheli
This paper presents a new approach to logic synthesis of digital synchronous circuits. We present a model
for synchronous circuits that supports logic transformations aimed at optimizing the circuit performance. Previous
synthesis approaches attacked this problem by separating the combinational logic from the registers and by applying
circuit transformations to the combinational component only. We show in this paper instead how to optimize
concurrently the circuit equations and the register position by a set of algorithms based on logic transformations.
390.
Description Logic Programs: Combining Logic Programs with Description Logic
- Benjamin N. Grosof,Ian Horrocks,Raphael Volz,Stefan Decker
We show how to interoperate, semantically and inferentially, between
the leading Semantic Web approaches to rules (RuleML
Logic Programs) and ontologies (OWL/DAML+OIL Description
Logic) via analyzing their expressive intersection. To do so, we define
a new intermediate knowledge representation (KR) contained
within this intersection: Description Logic Programs (DLP), and
the closely related Description Horn Logic (DHL) which is an expressive
fragment of first-order logic (FOL). DLP provides a significant
degree of expressiveness, substantially greater than the RDFSchema
fragment of Description Logic.
391.
From Process Logic to Program Logic
- Queen Mary London
We present a process logic for the p-calculus with the linear/affine
type discipline [6, 7, 31, 32, 33, 59, 60]. Built on the preceding
studies on logics for programs and processes, simple systems of
assertions are developed, capturing the classes of behaviours ranging
from purely functional interactions to those with destructive
update, local state and genericity. A central feature of the logic
is representation of the behaviour of an environment as the dual
of that of a process in an assertion, which is crucial for obtaining
compositional proof systems. From the process logic we can
derive compositional program logics for various higher-order programming
languages, whose soundness is proved via their...
392.
Da teoria russelliana das descrições ao atomismo lógico do \'Tractatus\' de Wittgenstein
- Vanice Ribeiro da Silva
A presente pesquisa pretende analisar o período do pensamento filosófico de B. Russell e L. Wittgenstein entre os anos de 1905 e 1914 descrevendo o desenvolvimento da filosofia do atomismo lógico presente no Tractatus logico-philosophicus de Wittgenstein. Para tanto, será observada a crítica deste à teoria do juízo desenvolvida por Russell, a qual seria fundamento para a teoria do conhecimento que o último elaborava. Reconhecemos, com base nas críticas, que Russell sofria uma forte influência do empirismo de sua época, o que tornou sua epistemologia frágil. Essa fragilidade é evidenciada por Wittgenstein, que, ao criticar alguns pontos fundamentais da teoria...
393.
On the Search for a Finitizable Algebraization of First Order Logic
- Ildikó Sain
We give an algebraic version of first order logic without equality in which the class of representable algebras forms a finitely based equational class. Further, the representables are defined in terms of set algebras, and all operations of the latter are permutation invariant. The algebraic form of this result is Theorem 1 (a concrete version of which is given by Theorems 1.8 and 3.2), while its logical form is Corollary 4.2. For first order logic with equality we give a result weaker than the one for first order logic without equality. Namely, in this case --- instead of finitely axiomatizing...
394.
A New Fixed-Point Theorem for Logic Programming Semantics
- Pascal Hitzler And; Pascal Hitzler; Anthony K. Seda
We present a new fixed-point theorem akin to the Banach contraction mapping theorem, but in the context of a novel notion of generalized metric space, and show how it can be applied to analyse the denotational semantics of certain logic programs. The theorem is obtained by generalizing a theorem of Priess-Crampe and Ribenboim, which grew out of applications within valuation theory, but is also inspired by a theorem of S.G. Matthews which grew out of applications to conventional programming language semantics. The class of programs to which we apply our theorem was defined previously by us in terms of operators...
395.
Connection Methods in Linear Logic and Proof Nets Construction
- D. Galmiche
Linear logic (LL) is the logical foundation of some type-theoretic languages and also of environments for specification and theorem proving. In this paper, we analyse the relationships between the proof net notion of LL and the connection notion used for efficient proof-search in different logics. Aiming at using proof nets as a tool for automated deduction in linear logic, we define a connection-based characterization of provability in Multiplicative Linear Logic (MLL). We show that an algorithm for proof net construction can be seen as a proof-search connection method. This central result is illustrated with a specific algorithm that is able...
396.
Infinitary Default Logic for Specification of Nonmonotonic Reasoning
- Joeri Engelfriet; V. Wiktor Marek; Jan Treur; Miroslaw Truszczy'nski
In this paper we study constructions leading to the formation of belief sets by agents. We focus on the situation when possible belief sets are built incrementally in stages. We call an infinite sequence of theories that represents such a process a reasoning trace. A set of reasoning traces describing all possible reasoning scenarios for the agent is called a reasoning frame. Default logic by Reiter is not powerful enough to represent reasoning frames. In the paper we introduce a generalization of default logic of Reiter by allowing infinite sets of justifications. We call this formalism infinitary default logic. In...
397.
A New Fixed-Point Theorem for Logic Programming Semantics
- Pascal Hitzler; Anthony K. Seda
We present a new fixed-point theorem akin to the Banach contraction mapping theorem, but in the context of a novel notion of generalized metric space, and show how it can be applied to analyse the denotational semantics of certain logic programs. The theorem is obtained by generalizing a theorem of Priess-Crampe and Ribenboim, which grew out of applications within valuation theory, but is also inspired by a theorem of S.G. Matthews which grew out of applications to conventional programming language semantics. The class of programs to which we apply our theorem was defined previously by us in terms of operators...
398.
A Description Logic with Concrete Domains and a Role-forming Predicate Operator
- Volker Haarslev; Carsten Lutz; Ralf Möller
This article presents the description logic ALCRP(D) with concrete domains and a roleforming predicate operator as its prominent aspects. We demonstrate the feasibility of ALCRP(D) for reasoning about spatial objects and their qualitative spatial relationships and provide an appropriate concrete domain for spatial objects. The general significance of ALCRP(D) is demonstrated by adding temporal reasoning to spatial and terminological reasoning using a combined concrete domain. The theory is motivated as a basis for knowledge representation and query processing in the domain of geographic information systems. In contrast to existing work in this domain, which mainly focuses either on conceptual reasoning...
399.
Infinitary Default Logic for Specification of Nonmonotonic Reasoning
- Joeri Engelfriet; V. Wiktor; Marek Jan Treur
In this paper we study constructions leading to the formation of belief sets by agents. We focus on the situation when possible belief sets are built incrementally in stages. We call an infinite sequence of theories that represents such a process a reasoning trace. A set of reasoning traces describing all possible reasoning scenarios for the agent is called a reasoning frame. Default logic by Reiter is not powerful enough to represent reasoning frames. In the paper we introduce a generalization of default logic of Reiter by allowing infinite sets of justifications. We call this formalism infinitary default logic. In...
400.
Differential-Algebraic Dynamic Logic for Differential-Algebraic Programs
- André Platzer
Abstract. We generalise dynamic logic to a logic for differential-algebraic programs, i.e., discrete programs augmented with first-order differentialalgebraic formulas as continuous evolution constraints in addition to first-order discrete jump formulas. These programs characterise interacting discrete and continuous dynamics of hybrid systems elegantly and uniformly. For our logic, we introduce a calculus over real arithmetic with discrete induction and a new differential induction with which differential-algebraic programs can be verified by exploiting their differential constraints algebraically without having to solve them. We develop the theory of differential induction and differential refinement and analyse their deductive power. As a case study, we...
