Wyniki wyszukiwania - BazTech

1

Justifications in Constraint Handling Rules for Logical Retraction in Dynamic Algorithms : Theory, Implementations, and Complexity

Frühwirth Thom

Fundamenta Informaticae

|

2020

|

Vol. 173, nr 4

253--283

EN

We present a concise source-to-source transformation that introduces justifications for user-defined constraints into the rule-based Constraint Handling Rules (CHR) programming language. There is no need to introduce a new semantics for justifications. This leads to a conservative extension of the language, as we can show the equivalence of rule applications. A scheme of two rules suffices to allow for logical retraction (deletion, removal) of CHR constraints during computation. Without the need to recompute from scratch, these rules remove the constraint and also undo all its consequences. We prove a confluence result concerning the rule scheme. We prove its correctness in general and tighten the results for confluent programs. We give an implementation, show its correctness, present two classical examples of dynamic algorithms, and improve the implementation. The computational overhead of introducing justifications and of performing logical retraction, i.e. the additional time and space needed, is proportional to the derivation length in the original program. This overhead may increase space complexity, but does not change the worst-case time complexity.

2

A Logic-Based, Reactive Calculus of Events

Chesani F., Mello P., Montali M., Torroni P.

Fundamenta Informaticae

|

2011

|

Vol. 105, nr 1/2

135-161

EN

Since its introduction, the Event Calculus (EC) has been recognized for being an excellent framework to reason about time and events, and it has been applied to a variety of domains. However, its formalization inside logic-based frameworks has been mainly based on backward, goal-oriented reasoning: given a narrative (also called execution trace) and a goal, logic-based formalizations of EC focus on proving the goal, i.e., establishing if a property (called fluent) holds. These approaches are therefore unsuitable in dynamic environments, where the narrative typically evolves over time: indeed, each occurrence of a new event requires to restart the reasoning process from scratch. Ad-hoc, procedural methods and implementations have been then proposed to overcome this issue. However, they lack a strong formal basis and cannot guarantee formal properties. As a consequence, the applicability of EC has been somehow limited in large application domains such as run-time monitoring and event processing, which require at the same time reactivity features as well as formal properties to provide guarantees about the computed response. We overcome the highlighted issues by proposing a Reactive and logic-based axiomatization of EC, called REC, on top of the SCIFF Abductive Logic Programming framework. Our solution exhibits the features of a reactive verification facility, while maintaining a solid formal background.

3

Principles of constrain systems and constraint solvers

Fruhwirth T., Abdennadher S.

Archives of Control Sciences

|

2006

|

Vol. 16, no. 2

131-159

EN

In this compact overview, we introduce the most common constraint system used in constraint programming lanquages and algorithms to solve them. Constraint systems are the result of taking a data type together with its operations and interpreting the resulting expressions as constraints. These constraint systems use the universal data types of numbers to represent scalar data or terms to represent structured data. Algorithms are presented as logical inference rules that are directly executable in the Constraint Handling Rules language.