Converting Constraint Handling Rules to Equivalent Transformation Rules

2006 ◽  
Vol 10 (3) ◽  
pp. 339-348 ◽  
Author(s):  
Yoshinori Shigeta ◽  
◽  
Kiyoshi Akama ◽  
Hiroshi Mabuchi ◽  
Hidekatsu Koike ◽  
...  
Keyword(s):  
Constraint Handling ◽  
Equivalent Transformation ◽  
Model Computation ◽  
Computation Model ◽  
Knowledge Processing ◽  
First Order ◽  
Transformation Rules ◽  
Logical Equivalence

We present a way to convert constraint handling rules (CHRs) to equivalent transformation rules (ETRs) and demonstrate the correctness of the conversion in equivalent transformation (ET) theory. In the ET computation model, computation is regarded as equivalent transformations of a description. A description is transformed successively by ETRs. Extensively used in the domain of first-order terms, the ET computation model has also been applied to knowledge processing in such data domains as RDF, UML, and XML. A CHR is a multiheaded guarded rule that rewrites constraints into simpler ones until they are solved. CHRs and ETRs are similar in syntax but they have completely different theoretical bases for the correctness of their computation. CHRs are based on the logical equivalence of logical formulas, while ETRs are based on the set equivalence of descriptions. We convert CHRs to rules used in the ET model and demonstrate converted rules to be correct ETRs, i.e., they preserve meanings of descriptions. We discuss correspondences and differences between CHRs and ETRs in theories, giving examples of correct ETRs that cannot be represented as CHRs.

How to Make Programs from Problem Descriptions in the Equivalent Transformation Paradigm

2003 ◽  
Vol 7 (3) ◽  
pp. 260-267
Author(s):  
Takahiko Ishikawa ◽  
◽  
Kiyoshi Akama ◽  
Hiroshi Mabuchi ◽  
◽  
...  
Keyword(s):  
Problem Solving ◽  
Expressive Power ◽  
Equivalent Transformation ◽  
Sample Problem ◽  
Computation Model ◽  
Transformation Rules ◽  
Manipulative Techniques

In the computation model of equivalent transformation (ET), problems are expressed by some declarative descriptions. Programs, which consist of equivalent transformation rules (ETRs), are made from the declarative descriptions, and applied to questions to solve them. The ET model can achieve various and efficient ways of problem-solving mainly due to the expressive power and priorities of ETRs. In this paper, we investigate and demonstrate, by solving a sample problem, how to make programs from problem descriptions in the ET paradigm. We introduce basic methods of generation and improvement of rules seeking for desirable ETRs. We can transform ETRs, preserving correctness of computation, through many manipulative techniques, i.e., changing from nondeterministic atoms into sequentially executable atoms, introducing multi-head rules, and adjusting priority of rules, by which we can effectively improve correct programs into both correct and more efficient programs.

Integration of Syntactic Analysis and Semantic Interpretation Based on Equivalent Transformation

2003 ◽  
Vol 7 (3) ◽  
pp. 306-314
Author(s):  
Hiroshi Mabuchi ◽  
◽  
Kiyoshi Akama ◽  
Takahiko Ishikawa ◽  
Hidekatsu Koike ◽  
...  
Keyword(s):  
General Principle ◽  
Efficient Algorithm ◽  
Semantic Interpretation ◽  
Cooperative Interaction ◽  
Syntactic Analysis ◽  
Equivalent Transformation ◽  
Language Understanding ◽  
Knowledge Processing ◽  
Transformation Rules ◽  
Mutually Independent

Making an efficient algorithm for natural language understanding by means of flexible and cooperative interaction between syntactic analysis and semantic interpretation is very difficult. In order to overcome the difficulties, the present paper proposes a new method for designing knowledge processing systems, the computation of which is based on equivalent transformation of declarative descriptions. Basic procedures for syntactic analysis and semantic interpretation are formalized as mutually independent equivalent transformation rules. Rule selection is dynamically determined flexibly during execution by a general principle independent of the domain of sentences.

scholarly journals Design of Nondeterministic Program Termination Based on the Equivalent Transformation Computation Model

2006 ◽  
Vol 10 (3) ◽  
pp. 349-361
Author(s):  
Itaru Takarajima ◽  
◽  
Kiyoshi Akama ◽  
Ikumi Imani ◽  
Hiroshi Mabuchi ◽  
...  
Keyword(s):  
Programming Languages ◽  
Program Synthesis ◽  
Equivalent Transformation ◽  
Sufficient Condition ◽  
Model Computation ◽  
Computation Model ◽  
Program Termination ◽  
Nondeterministic Program

We studied the termination of nondeterministic programs, which play an important, basic role in program synthesis, and provide a foundation for proving program termination. The class of programs we consider here is based on the <I>equivalent transformation (ET)</I> computation model. Computation with this model involves the succesive application of rules to sets of clauses. Since the ET model has more expressive terms and rules than other programming languages, program termination is difficult to prove: we must take into account all possible changes of terms made by various rules. We propose a sufficient condition of ET program termination that proves termination by checking each rule in a given program. We also provide an algorithm for this check.

Formalization of the Equivalent Transformation Computation Model

2006 ◽  
Vol 10 (3) ◽  
pp. 245-259 ◽  
Author(s):  
Kiyoshi Akama ◽  
◽  
Ekawit Nantajeewarawat ◽  
Keyword(s):  
Program Synthesis ◽  
Background Knowledge ◽  
Basic Structure ◽  
Equivalent Transformation ◽  
Computation Model ◽  
Problem Domain ◽  
Central Importance ◽  
Program Correctness ◽  
Transformation Rules ◽  
Successive Reduction

In the equivalent transformation (ET) computation model, a specification provides background knowledge in a problem domain and defines a set of queries of interest. A program is a set of prioritized transformation rules, and computation consists in successive reduction of queries using meaning-preserving transformation with respect to given background knowledge. We present a formalization of the ET model from the viewpoint of program synthesis, where not only computation but also program correctness and correctness relations are of central importance. The notion of program correctness defines “what it means for a program to be correct with respect to a specification,” and a correctness relation provides guidance on “how to obtain such a program.” The correctness relation of the ET model is established, based on which how the basic structure of the ET model facilitates program synthesis is discussed together with program synthesis strategies in this model.

scholarly journals Program Verification using Constraint Handling Rules and Array Constraint Generalizations

10.29007/dkxs ◽  
2018 ◽  
Author(s):  
Emanuele De Angelis ◽  
Fabio Fioravanti ◽  
Alberto Pettorossi ◽  
Maurizio Proietti
Keyword(s):  
Data Structures ◽  
Program Verification ◽  
Linear Constraints ◽  
Constraint Handling ◽  
Logic Programs ◽  
Replacement Strategy ◽  
Partial Correctness ◽  
Transformation Rules ◽  
Constraint Logic Programs ◽  
Additional Constraints

The transformation of constraint logic programs (CLP programs)has been shown to be an effective methodologyfor verifying properties of imperative programs.By following this methodology, we encode the negationof a partial correctness property of an imperativeprogram prog as a predicate incorrect defined by a CLP program P, and we show thatprog is correct by transforming P intothe empty program through the applicationof semantics preserving transformation rules.Some of these rules perform replacements of constraintsthat encode properties of the data structures manipulatedby the program prog.In this paper we show that Constraint Handling Rules (CHR)are a suitable formalism for representing and applyingconstraint replacements during the transformation of CLP programs.In particular, we consider programs that manipulate integerarrays and we present a CHR encoding of a constraint replacementstrategy based on the theory of arrays.We also propose a novel generalization strategy forconstraints on integer arrays that combinesthe CHR constraint replacement strategywith various generalization operator for linear constraints,such as widening and convex hull.Generalization is controlled by additional constraintsthat relate the variable identifiers in the imperativeprogram and the CLP representation of their values.The method presented in this paper has been implemented andwe have demonstrated itseffectiveness on a set ofbenchmark programs taken from the literature.

Knowledge Processing Using EKRL for Robotic Applications

2017 ◽  
Vol 11 (4) ◽  
pp. 1-21 ◽  
Author(s):  
Omar Adjali ◽  
Amar Ramdane-Cherif
Keyword(s):  
Probabilistic Reasoning ◽  
Markov Logic Networks ◽  
Knowledge Processing ◽  
Markov Logic ◽  
Semantic Framework ◽  
First Order ◽  
Knowledge Representation Language ◽  
Representation Language ◽  
Robotic Applications ◽  
Model Environment

This article describes a semantic framework that demonstrates an approach for modeling and reasoning based on environment knowledge representation language (EKRL) to enhance interaction between robots and their environment. Unlike EKRL, standard Binary approaches like OWL language fails to represent knowledge in an expressive way. The authors show in this work how to: model environment and interaction in an expressive way with first-order and second-order EKRL data-structures, and reason for decision-making thanks to inference capabilities based on a complex unification algorithm. This is with the understanding that robot environments are inherently subject to noise and partial observability, the authors extended EKRL framework with probabilistic reasoning based on Markov logic networks to manage uncertainty.

Fuzzy-Random FOSM and its Application in Low Cycle Fatigue Life Reliability Analysis of an Aeronautical Engine Turbine Disk

2006 ◽  
Vol 324-325 ◽  
pp. 775-778 ◽  
Author(s):  
You Liang Xu ◽  
Cheng Li Liu ◽  
Zhen Zhou Lu
Keyword(s):  
Fatigue Life ◽  
Reliability Analysis ◽  
Low Cycle Fatigue ◽  
Equivalent Transformation ◽  
Possibility Distribution ◽  
First Order ◽  
Random Uncertainty ◽  
Random Probability ◽  
Second Moment Method ◽  
Fuzzy Random

An approximate analytical method is presented to analyze reliability for the structure with fuzzy-random uncertainty in basic variables. On the basis of equivalent transformation from fuzzy possibility distribution (FPD) to random probability distribution (RPD), this contribution expands first order and second moment method (FOSM) for random reliability to that for fuzzy-random reliability. The expanded FOSM is illustrated by the way of the fuzzy-random low fatigue life reliability analysis about an aeronautical engine disk affected by fuzzy-random uncertainty. Comparison between the FOSM and the numerical simulation for the fuzzy-random reliability demonstrates the precision of the presented computational model.

The model-companion of a class of structures

1972 ◽  
Vol 37 (3) ◽  
pp. 546-556 ◽  
Author(s):  
G. L. Cherlin
Keyword(s):  
Order Theory ◽  
Model Companion ◽  
Elementary Substructure ◽  
Closed Model ◽  
First Order ◽  
First Order Theory ◽  
Logical Equivalence ◽  
Closed Fields ◽  
Algebraically Closed Fields ◽  
Model Completion

If Σ is the class of all fields and Σ* is the class of all algebraically closed fields, then it is well known that Σ* is characterized by the following properties:(i) Σ* is the class of models of some first order theory K*.(ii) If m1m2 are in Σ* and m1 ⊆ m2 then m1 ≺ m2 (m1 is an elementary substructure of m2, i.e. any first order sentence true in m1 is true in m2).(iii) If m1 is in Σ then there is a structure m2 in Σ* such that m1 ⊆ m2.If Σ is some other class of models of a first order theory K and a subclass Σ* of Σ exists satisfying (i)–(iii) then Σ* is uniquely determined and K* (which is unique up to logical equivalence) is called the model-companion of K. This notion is a generalization of the fundamental notion of model-completion introduced and extensively studied by A. Robinson [6], When the model-companion exists it provides the basis for a satisfactory treatment of the notion of an algebraically closed model of K.Recently A. Robinson has developed a more general formulation of the notion of “algebraically closed” structures in Σ, which is applicable to any inductive elementary class Σ of structures (by elementary we always mean ECΔ). Condition (i) must be weakened to(i′) Σ* is closed under elementary substructure (i.e. if m1 is in Σ* and m2 ≺ m1 then m2 is in Σ*).

Sign in / Sign up

Export Citation Format

Share Document