Is The Success Of Fuzzy Logic Really Paradoxical? Or: Towards The Actual Logic Behind Expert Systems - Olga M. Kosheleva,Vladik Kreinovich
. The formal concept of logical equivalence in fuzzy logic
, while theoretically
sound, seems impractical. The misinterpretation of this concept has led to some
. Motivated by practical interpretation of truth values for fuzzy
propositions, we take the class (lattice) of all sub-intervals of the unit interval [0,1] as the
truth value space for fuzzy logic, subsuming the traditional class of numerical truth values
from [0,1]. The associated concept of logical equivalence is stronger than the traditional
one. Technically, we are dealing with much smaller set of pairs of equivalent formulas, so
that we are able to check equivalence algorithmically. The checking is done by showing
A Kernel of Data Structures and Algorithms for Automated Deduction with Equality Clauses - Jos'e Miguel Rivero,Robert Nieuwenhuis,Miguel Angel Vallejo
. We present Dedam (Deduction Abstact Machine), a standard
architecture around which high-performance theorem provers for
clausal logic with equality can be built. It includes a WAM-like heap
structure for storing terms as DAG's, several indexing data structures,
and mechanisms for efficient memory management and demodulation.
These data structures turn out to be surprisingly well combinable due
to conceptual similarities.
We provide statistics showing how we reduce two well-known bottlenecks
in equational deduction. The first one, matching for demodulation
is done by a new indexing method, substitution trees with equality
constraints. Regarding the other bottle neck, memory management,
WAM-based techniques allow us to completely avoid it during unification,
matching, and demodulation. Static...
Sequentiality, Monadic Second-Order Logic and Tree Automata - Hubert Comon
Given a term rewriting system R and a normalizable term t, a
redex is needed if in any reduction sequence of t to a normal form, this
redex will be contracted. Roughly, R is sequential if there is an optimal
reduction strategy in which only needed redexes are contracted. More
generally, G. Huet and J.-J. L'evy define in  the sequentiality of
a predicate P on partially evaluated terms. We show here that the
sequentiality of P is definable in SkS, the monadic second-order logic
with k successors, provided P is definable in SkS. We derive several
known an new consequences of this remark: 1--strong sequentiality, as
Metamorphosis: State Assignment by Retiming and Re-encoding - Balakrishnan Iyer,Maciej Ciesielski
This paper presents Metamorphosis
-- a novel technique for optimal state assignment targeting
multi-level logic implementations. We present a new formulation and synthesis techniques
for the state assignment problem based on controlled retiming and re-encoding of a symbolically
represented finite state machine (FSM) represented initially with a one-hot code. Metamorphosis
is a new design paradigm that integrates the structural and behavioral design methodologies in
a synergistic fashion and leverages the additional degrees of freedom to the synthesis of optimal
FSM. The proposed technique differs drastically from previous approaches in that the encoding
process is guided directly by the cost function (optimization criterion) rather than speculative
estimates of the encoding...
CLAM Specification for Provably Correct Compilation of - Egon B Orger,Rosario F. Salamone
The paper extends the correctness proof in  for compilation
of Prolog programs on the WAM to CLP(R) programs on the Constraint
Logic Arithmetic Machine (CLAM [8, 10]). This serves to
illustrate, through a complex case study, how the evolving algebra
specification methodology allows to incorporate modularity and extendability
principles in system design.
This paper extends, to the Constraint Logic Arithmetic Machine (CLAM)
and CLP(R) programs, the mathematical analysis of the Warren Abstract
Machine (WAM) for executing Prolog and the resulting correctness proof
for a general compilation scheme of Prolog to the WAM given in .
Starting from an abstract CLP(R) model---which paraphrases the primary
model for Prolog defined in...
Reasoning about Effects of Concurrent Actions - Chitta Baral,Gelfond Gelfond
this paper we extend the language A and
its translation to allow reasoning about the effects of concurrent actions.
The logic programming formalization of situation calculus with concurrent
actions presented in the paper is of independent interest and may serve
as a test bed for the investigation of various transformations and logic
programming inference mechanisms. !
Verifying Reachability in LOTOS Specifications by Temporal Logic - W. M. Mak,T. Y. Cheung,C. Lee
A method for verifying reachability properties of distributed system designs
specified in the formal description technique LOTOS is proposed. It consists of a
linear temporal propositional logic language and a compositional temporal semantics
with linear temporal operators. Based on this semantics, both the design specified in
LOTOS and its properties can be expressed as logical formulas. Proving the presence
of a property in the design is then equivalent to logically deducing the formula
representing the designated property from the formula representing the given LOTOS
specification. This paper emphasizes on the application of the method to proving that
the intended operations of a design are reachable. That is, they...
Supporting Data Integration and Warehousing Using H2O - Richard Hull,Roger King,Jean-claude Franchitti
This paper presents a broad framework for data integration, that supports both data materialization
and virtual view capabilities, and that can be used with legacy as well as modern database
systems. The framework is based on "integration mediators", these are software components that
use techniques generalized from active databases, such as triggering and rulebases. This permits
the logic, especially for incremental maintenance of materialized data, of an integration mediator
to be specified in a relatively declarative and modular fashion.
One specific focus of this paper is the development of a taxonomy of the solution space
for supporting and maintaining integrated views. A second focus concerns providing support
Representing Autoepistemic Introspection in Terms of Default Rules - Tomi Janhunen
This paper addresses the relationship of Reiter's default logic, Moore's autoepistemic logic as well as Marek and Truszczynski's strong autoepistemic logic from a new point of view. Earlier research results on their interconnection support the view that default reasoning is a special case of autoepistemic reasoning. To the contrary, this paper shows how autoepistemic theories can be faithfully translated into default theories. Consequently, autoepistemic reasoning can be seen a form of default reasoning. This indicates together with the previous research results that autoepistemic logic and default logic are of equal generality. As a practical application of the presented translation, it...
Restricting the hypothesis space, guiding the search, and handling the redundant information in Inductive Logic Programming - Uros Pompe
We developed and implemented an inductive logic programming system and the first order
classifier, called ILP-R. It is capable of efficiently inducing theories in a restricted subset
of function free normal programs. It is able to use the hypothesis to classify new instances,
by using the naive Bayesian reasoning. The contributions of the system are threefold.
First, we devised a weak syntactic declarative bias restricting the set of possible hypotheses.
We discuss and prove its properties. The latter are then exploited to encode
the current proof of a partially induced clause in such a way, that the encoding grows at
most linearly with respect to the clause...
F1.094e+06>The Journal of Functional and Logic Programming The MIT Press Volume 1998, Article 6
In this paper, we present an extension of the Ja#ar-Lassez constraint
logic programming scheme that operates with unions of constraint theories
with di#erent signatures and decides the satisfiability of mixed
constraints by appropriately combining the constraint solvers of the
component theories. We describe the extended scheme, and provide
logical and operational semantics for it along the lines of those given
for the original scheme. We then show how the main soundness and
completeness results of constraint logic programming lift to our extension.
The constraint logic programming (CLP) scheme was originally developed
by Ja#ar and Lassez [JL86] as a principled way to combine the computational
paradigms of logic programming and...
Developing Secure Applications: A Systematic Approach - C. Eckert,D. Marek
This paper presents parts of the SECREDS project which aims to bridge the
gap between system modeling and implementation using a high-level programming
language. Within SECREDS secure applications are developed top down
starting with a top-level specification. Top-level specifications are given by our
computational model and application-specific security policies are specified
using our security requirement logic. To implement a top-level specification
we developed a high-level programming language called INSEL
concepts well adapted to our underlying model. We will present main
features of INSEL
focusing on access control aspects and we will outline
some guidelines to support the systematic implementation of a given top-level
specification preserving specified security properties.
Access Control, Security...
TAO - A Model for the Integration of Concurrency and Synchronisation in Object-Oriented Programming - S. E. Mitchell
The integration of concurrency into inheritance has been attempted in a number of languages. However, some of the compromises made have seriously degraded the usefulness of these languages. Hence none of these languages have been totally successful. A particular problem has been the "inheritance anomaly" caused by interactions between synchronisation mechanisms and inheritance. This thesis introduces a new model, called TAO, for this integration. The model allows for (multiple) threads to be embedded in an object and provides details of how these threads are handled in inheritance. We also develop a new concurrency control mechanism, based on a combination of...
Specialised Recombinative Operators for Timetabling Problems - Edmund Burke,David Elliman,Rupert Weare
. This paper discusses a series of recombination operators for the timetabling problem. These operators act upon a direct representation of the timetable and maintain the property of feasibility. That is that there are no conflicts and no overfilled rooms. Various approaches to solving the timetabling problem using evolutionary computing methods are first compared. The recombination operators are then presented and various alternatives for incorporating heuristic knowledge in the search are described. Finally, results are presented comparing the operators on a real timetabling problem. 1 Introduction Recently, there has been a lot of attention paid to the problem of automating...
Oracles for Checking Temporal Properties of Concurrent Systems - Laura K. Dillon,Qing Yu
Verifying that test executions are correct is a crucial
step in the testing process. Unfortunately, it can be
a very arduous and error-prone step, especially when
testing a concurrent system. System developers can
therefore benefit from oracles automating the verification
of test executions.
This paper examines the use of Graphical Interval
Logic (GIL) for specifying temporal properties of concurrent
systems and describes a method for constructing
oracles from GIL specifications. The visually
intuitive representation of GIL specifications makes
them easier to develop and to understand than specifications
written in more traditional temporal logics.
Additionally, when a test execution violates a GIL
specification, the associated oracle provides information
about a fault. This information can be displayed
Specifying Filler-Gap Dependency Parsers in a Linear-Logic Programming Language - Joshua S. Hodas
An aspect of the Generalized Phrase Structure Grammar formalism proposed
by Gazdar, et al. is the introduction of the notion of "slashed categories
" to handle the parsing of structures, such as relative clauses, which
involve unbounded dependencies. This has been implemented in Definite
Clause Grammars through the technique of gap threading, in which a difference
list of extracted noun phrases (gaps) is maintained. However, this
technique is cumbersome, and can result in subtle soundness problems in
the implemented grammars. Miller and Pareschi have proposed a method of
implementing gap threading at the logical level in intuitionistic logic. Unfortunately
that implementation itself suffered from serious problems, which
the authors recognized....
ERTL: An Extension to RTL for Requirements Analysis for Hybrid Systems
this paper we
provide extensions to RTL which allow reasoning about absolute timings for both continuous and discrete
time, and reasoning about system behaviour in the value and time domains by parametrising predicates
in terms of system variables. Incorporating these features into RTL we obtain Extended Real-Time Logic
(ERTL) which is suitable for the modelling and analysis of hybrid systems.
The paper is organized as follows. In the next section we present the concepts of an event-action model,
and discuss their formalisation in terms of RTL and ERTL. Section 3 defines the syntax and semantics
of ERTL. Section 4 presents two case studies, the first is the...
Phased Logic: Supporting the Synchronous Design Paradigm with Delay--Insensitive Circuitry - Daniel H. Linder,James C. Harden
Phased logic is proposed as a solution to the increasing problem of timing complexity
in digital design. It is a delay--insensitive design methodology that seeks to restore the separation
between logical and physical design by eliminating the need to distribute low--skew clock
signals and carefully balance propagation delays. However, unlike other methodologies that avoid
clocks, phased logic supports the cyclic, deterministic behavior of the synchronous design paradigm.
This permits the designer to rely chiefly on current experience and CAD tools to create
phased logic systems. Marked graph theory is used as a framework for governing the interaction
of phased logic gates that operate directly on Level--Encoded two--phase...
Answer Sets in General Nonmonotonic Reasoning (Preliminary Report) - Vladimir Lifschitz,Thomas Y. C. Woo
Languages of declarative logic programming
differ from other modal nonmonotonic formalisms
by lack of syntactic uniformity. For
instance, negation as failure can be used in
the body of a rule, but not in the head; in
disjunctive programs, disjunction is used in
the head of a rule, but not in the body; in extended
programs, negation as failure can be
used on top of classical negation, but not the
other way around. We argue that this lack
of uniformity should not be viewed as a distinguishing
feature of logic programming in
general. As a starting point, we take a translation
from the language of disjunctive programs
with negation as failure and classical
negation into MBNF---the...
Combining Temporal Logic Systems - Marcelo Finger,Dov Gabbay
This paper is a continuation of the work started in [FG92] on combining temporal
logics. In this work, four combination methods are described and studied with respect
to the transference of logical properties from the component one-dimensional temporal
logics to the resulting two-dimensional temporal logic. Three basic logical properties
are analysed, namely soundness, completeness and decidability.
Each combination method is composed of three submethods that combine the languages,
the inference systems and the semantics of two one-dimensional temporal logic
systems, generating families of two-dimensional temporal languages with varying expressivity
and varying degree of transference of logical properties. The temporalisation
method and the independent combination method are shown to transfer...