Dialectical argumentation to solve conflicts in advice giving: a case study in the promotion of healthy nutrition

Conflict situations do not only arise from misunderstandings, erroneous perceptions, partial knowledge, false beliefs, etc., but also from differences in “opinions” and in the different agents' value systems. It is not always possible, and maybe not even desirable, to “solve” this kind of conflict, as the sources are subjective. The communicating agents can, however, use knowledge of the opponent's preferences, to try and convince the partner of a point of view which they wish to promote. To deal with these situations requires an argumentative capacity, able to handle not only “demonstrative” arguments but also “dialectic” ones, which may not necessarily be based on rationality and valid premises. This paper presents a formalization of a theory of informal argumentation, focused on techniques to change attitudes of the interlocutor, in the domain of health promotion.     

Multi-perspective Navigation of Movies

Digital libraries of video are rapidly growing in size and availability through digital networks of computers. The explosion of digital unstructure information, such as video, traveling through the network raises the need for tools that allow video information structuring and “intelligent” access to sequences.In this paper we present a novel video database system, which has been expressly designed to support structured storage of movies. A semiotic formalization for movie logical organization is here introduced and exploited to derive the conceptual schema of an object-oriented movie database. This structure is expressly tailored to enable queries on film technical features and on semantic contents as well, thus allowing feature fusion and access from multiple perspectives. A novel visual interaction scheme is implemented that allows users to formulate queries as filtering operations, that enable focussing on the interesting part of information, while skipping the rest. Formalization of the operators of “perspective” and “filtering” is thereby supplied. Retrieval of stored sequences by iconic motion example is also implemented for accessing sequences by contents. Examples are supplied of interaction with the database and of expressive power of visual query language.     

A verified Common Lisp implementation of Buchberger’s algorithm in ACL2

In this article, we present the formal verification of a Common Lisp implementation of Buchberger’s algorithm for computing Gröbner bases of polynomial ideals. This work is carried out in ACL2, a system which provides an integrated environment where programming (in a pure functional subset of Common Lisp) and formal verification of programs, with the assistance of a theorem prover, are possible. Our implementation is written in a real programming language and it is directly executable within the ACL2 system or any compliant Common Lisp system. We provide here snippets of real verified code, discuss the formalization details in depth, and present quantitative data about the proof effort.     

A logic for reasoning about probabilities

We consider a language for reasoning about probability which allows us to make statements such as “the probability of E₁ is less than ” and “the probability of E₁ is at least twice the probability of E₂,” where E₁ and E₂ are arbitrary events. We consider the case where all events are measurable (i.e., represent measurable sets) and the more general case, which is also of interest in practice, where they may not be measurable. The measurable case is essentially a formalization of (the propositional fragment of) Nilsson's probabilistic logic. As we show elsewhere, the general (nonmeasurable) case corresponds precisely to replacing probability measures by Dempster-Shafer belief functions. In both cases, we provide a complete axiomatization and show that the problem of deciding satisfiability is NP-complete, no worse than that of propositional logic. As a tool for proving our complete axiomatizations, we give a complete axiomatization for reasoning about Boolean combinations of linear inequalities, which is of independent interest. This proof and others make crucial use of results from the theory of linear programming. We then extend the language to allow reasoning about conditional probability and show that the resulting logic is decidable and completely axiomatizable, by making use of the theory of real closed fields.     

Distributed Event Graphs: Formalizing Component-based Modelling and Simulation

In this work an extension to the classical Event Graphs formalism for discrete-event simulation is presented. The extensions are oriented towards the specification of component-based models. The abstract syntax has been defined through meta-modelling. Several methodological issues are discussed, concerning the use of two different meta-modelling levels or collapsing the language into a single one, where “instance-of” relationships are used between processes and their classes. The operational semantics have been defined through graph transformation. This formal definition enables analysis before code is generated from the model. The syntax and semantics of the visual language have been implemented in the multi-paradigm tool AToM³, together with a code generator that produces stand-alone applications able to run the analysed models in real-time.     

Invariant computations for analytic projective geometry

This paper focuses on two underlying questions for symbolic computations in projective geometry:

I How should a projective geometric property be written analytically? A first order formula in the language of fields which expresses a “projective geometric property” is translated, by an algorithm, into a restricted class of formulas in the analytic geometric language of brackets (or invariants). This special form corresponds to statements in synthetic projective geometry and the algorithm is a basic step towards translation back into synthetic geometry.

II How are theorems of analytic geometry proven? Axioms for the theorems of analytic projective geometry are given in the invariant language. Identities derived form Hubert's Nullstellensatz then play a central role in the proof. Prom a proof of an open theorem about “geometric properties”, over all fields, or over ordered fields, an algorithm derives Nullstellensatz identities — giving maximal algebraic simplicity, and maximal information in the proof.

The results support the proposal that computational analytic projective geometry should be carried out directly with identities in the invariant language.     

Performance analysis of GAME: A generic automated marking environment

This paper describes the Generic Automated Marking Environment (GAME) and provides a detailed analysis of its performance in assessing student programming projects and exercises. GAME has been designed to automatically assess programming assignments written in a variety of languages based on the “structure” of the source code and the correctness of the program’s output. Currently, the system is able to mark programs written in Java, C++ and the C language. To use the system, instructors are required to provide a simple “marking schema” for each given assessment item, which includes pertinent information such as the location of files and the model solution. In this research, GAME has been tested on a number of student programming exercises and assignments and its performance has been compared against that of a human marker. An in-depth statistical analysis of the comparison is presented, providing encouraging results and directions for employing GAME as a tool for teaching and learning.     

The Rewriting Logic Semantics Project

Rewriting logic is a flexible and expressive logical framework that unifies denotational semantics and SOS in a novel way, avoiding their respective limitations and allowing very succinct semantic definitions. The fact that a rewrite theory's axioms include both equations and rewrite rules provides a very useful “abstraction knob” to find the right balance between abstraction and observability in semantic definitions. Such semantic definitions are directly executable as interpreters in a rewriting logic language such as Maude, whose generic formal tools can be used to endow those interpreters with powerful program analysis capabilities.     

An Overview of Cαml

Cαml is a tool that turns a so-called “binding specification” into an Objective Caml compilation unit. A binding specification resembles an algebraic data type declaration, but also includes information about names and binding. Cαml is meant to help writers of interpreters, compilers, or other programs-that-manipulate-programs deal with α-conversion in a safe and concise style. This paper presents an overview of Cαml's binding specification language and of the code that Cαml produces.     

Coinductive Verification of Program Optimizations Using Similarity Relations

Formal verification methods have gained increased importance due to their ability to guarantee system correctness and improve reliability. Nevertheless, the question how proofs are to be formalized in theorem provers is far from being trivial, yet very important as one needs to spend much more time on verification if the formalization was not cleverly chosen. In this paper, we develop and compare two different possibilities to express coinductive proofs in the theorem prover Isabelle/HOL. Coinduction is a proof method that allows for the verification of properties of also non-terminating state-transition systems. Since coinduction is not as widely used as other proof techniques as e.g. induction, there are much fewer “recipes” available how to formalize corresponding proofs and there are also fewer proof strategies implemented in theorem provers for coinduction. In this paper, we investigate formalizations for coinductive proofs of properties on state transition sequences. In particular, we compare two different possibilities for their formalization and show their equivalence. The first of these two formalizations captures the mathematical intuition, while the second can be used more easily in a theorem prover. We have formally verified the equivalence of these criteria in Isabelle/HOL, thus establishing a coalgebraic verification framework. To demonstrate that our verification framework is suitable for the verification of compiler optimizations, we have introduced three different, rather simple transformations that capture typical problems in the verification of optimizing compilers, even for non-terminating source programs.     

Mixing Two Bibliography Style Languages

This article reports a twofold experience. On the one hand, we show that some concepts related to xml can be used to define a language for formatting a bibliography section put at the end of a printed work. On the second hand, we show that this new language can be used jointly with the bibliography style language of BIBT_EX in the new version of MlBIBT_EX. This should ease the transition between the “old” bibliography style language and the “new” one.     

A denotational theory of synchronous reactive systems

In this paper, systems which interact permanently with their environments are considered. Such systems are encountered, for instance, in real-time control or signal processing systems, C³-systems, and man-machine interfaces, to mention just a few cases. The design and implementation of such systems require a concurrent programming language which can be used to verify and synthesize the synchronization mechanisms, and to perform transformations of the concurrent source code to match a particular target architecture. Synchronous languages are convenient tools for such a purpose: they rely on the assumptions that: (1) internal actions of synchronous systems are instantaneous, and (2) communication with the environment is performed via instantaneous flashes involving some external stimuli. In this paper, we present a mathematical model of synchronous languages and illustrate its use on the language. This model is denotational, and encompasses both relational and functional styles of specification. It allows us to answer fundamental questions related to synchronous languages, such as “what are the basic constructions which should be provided by such languages?”     

Formal compiler construction in a logical framework

The task of designing and implementing a compiler can be a difficult and error-prone process. In this paper, we present a new approach based on the use of higher-order abstract syntax and term rewriting in a logical framework. All program transformations, from parsing to code generation, are cleanly isolated and specified as term rewrites. This has several advantages. The correctness of the compiler depends solely on a small set of rewrite rules that are written in the language of formal mathematics. In addition, the logical framework guarantees the preservation of scoping, and it automates many frequently-occurring tasks including substitution and rewriting strategies. As we show, compiler development in a logical framework can be easier than in a general-purpose language like ML, in part because of automation, and also because the framework provides extensive support for examination, validation, and debugging of the compiler transformations. The paper is organized around a case study, using the MetaPRL logical framework to compile an ML-like language to Intel x86 assembly. We also present a scoped formalization of x86 assembly in which all registers are immutable.     

子程序花指令模糊变换逻辑一致性研究

花指令模糊变换是代码模糊变换策略中的一种有效方法.在分析现有花指令加密方法的基础上,提出一种子程序花指令模糊变换方案,并利用形式化方法对其进行描述.通过研究子程序花指令模糊变换各种形式化的定义,推导出若干引理,从"XOR及CMP扩展"、"伪分支构造"、"JNE后加花指令"等3个方面加以形式化的证明,使得经上述子程序花指令模糊变换的程序具有与原程序相同的逻辑性.最后,以代码模糊变换评测标准对该算法的效果进行了详细分析.     

花指令模糊变换逻辑一致性研究

花指令模糊变换是代码模糊变换策略中的一种有效方法。在分析现有花指令加密方法的基础上，给出一种随机花指令模糊变换加密方案，并利用形式化方法对其进行了描述。通过研究花指令模糊变换各种形式化的定义，推导出若干引理，从“JMP扩展”、“JMC变换”、“JMP后添加花指令”等3个方面形式化地证明了经上述随机花指令加密算法变换的程序具有与原始程序相同的逻辑性。     

Conversation rebuilding: From the foreign language classroom to implementation in an intelligent tutoring system

This paper shows how an innovative “communicative” technique in teaching foreign languages—Conversation Rebuilding (CR)—readily lends itself to implementation in an Intelligent Tutoring System (ITS). Classroom language teachers using CR get students to formulate acceptable utterances in a foreign idiom by starting from rough approximations (using words the students know) and gradually zeroing in on the utterance which a native speaker of that idiom might produce in a similar setting. The ITS presented here helps students do the “zeroing in” optimally. It lets them express themselves temporarily in an “interlingua” (i.e., in their own kind of French or English or whatever they are studying), as long as they make something of their communicative intent clear, that is, as long as the System can find a semantic starting point on which to build. The ITS then prods the students to express themselves more intelligibly, starting from the “key” elements (determined by a heuristic based on how expert classroom teachers proceed) and taking into consideration the students' past successful or unsuccessful attempts at communication. To simplify system design and programming, however, conversations are “constrained”: students playact characters in set dialogs and aim at coming up with what the characters actually say (not what they could possibly say). While most Intelligent Computer Assisted Language Learning (ICALL) focuses the attention of students on norms to acquire, the ICALL implementation of CR presented in this paper focuses the attention of students on saying something—indeed, almost anything—to keep the conversation going and get some kind of meaning across to the other party. It sees successful language acquisition primarily as the association of forms with intent, not simply as the conditioning of appropriate reflexes or the elaboration/recall of conceptualized rules (which are the by-products of successful communication). Thus, in espousing this hard-line communicative approach, the present paper makes a first, non-trivial point: ICALL researchers might usefully begin by investigating what the more able teachers are doing in the classroom, rather than by building elaborate computer simulations of out-dated practices, as happens all too often. The paper then goes on to describe the architecture of a prototype ITS based on CR—one that the authors have actually implemented and tested—for the acquisition of English as a foreign language. A sample learning session is transcribed to illustrate the man-machine interaction. Concluding remarks show how the present-day limits of ICALL (and Artificial Intelligence in general) can be partially circumvented by the strategy implemented in the program, i.e. by making the students feel they are creatively piloting an interaction rather than being tested by an unimaginative machine.     

prialt in Handel-C: an operational semantics

We describe an operational semantics for the hardware compilation language Handel-C [7], which is a C-like language with channel communication and parallel constructs which compiles down to mainly synchronously clocked hardware. The work in this paper builds on previous work describing the semantics of the “prialt” construct within Handel-C [5] and a denotational semantics for part of the language [6]. We describe a key subset of the language and show how a design decision for the real language, namely that default guards in a prialt statement executed in “zero-time”, has consequences for the complexity of the operational semantics. We present the operational semantics, along with a revised and completed prialt semantics, indicating clearly the interface between them. We then describe a notion of observational equivalence and present an example illustrating how we handle the complexity of nested prialts in default guards.     

No-Longer-Foreign: Teaching an ML compiler to speak C “natively”

We present a new foreign-function interface for SML/NJ. It is based on the idea of data-level interoperability—the ability of ML programs to inspect as well as manipulate C data structures directly.The core component of this work is an encoding of the almost² complete C type system in ML types. The encoding makes extensive use of a “folklore” typing trick, taking advantage of ML's polymorphism, its type constructors, its abstraction mechanisms, and even functors. A small low-level component which deals with C struct and union declarations as well as program linkage is hidden from the programmer's eye by a simple program-generator tool that translates C declarations to corresponding ML glue code.