361.
Computational Logic in Australia
interpretation is a language-independent
theory for static analysis of programs. This theory
plays a prominent role in much work in the group,
since most sophisticated implementation ideas require
static analysis. The work contributes to the theory
generally, as well as its applications in functional and
logic programming, including sophisticated program
transformation.
Techniques are also being developed to dramatically
reduce the time and effort spent on debugging.
Traditional debugging techniques are based on following
the steps of program execution. With high-level
languages such as logic programming languages, the
sequence of execution steps can be very complex.
Declarative debugging is an interactive technique
that pinpoints errors using programmers' responses to
queries. The program, as a logical description of...
362.
Omega-Restricted Logic Programs
We define a new syntactic class of logic programs, omega-restricted programs. We divide the predicate symbols of a logic program into two parts: domain and non-domain predicates, where the domain predicates are defined by the maximal stratifiable subset of the rules of the program. We extend the usual de nition of stratification by adding a special omega-stratum that holds all unstratifiable predicates of the program. We demand that all variables that occur in a rule also occur in the rule body in a positive literal that is on a lower stratum than rule head. This restriction is syntactic and can...
363.
Layout-driven Logic Optimization
With the advent of deep sub-micron technologies, interconnect loads
and delays are becoming dominant. Consequently, the currently used
design flow of iteratively performing logic synthesis with statistical
wire-load models, doing placement & routing, extracting parasitics,
and using them back in the synthesis tool runs into serious timing
convergence problems. Layout-driven synthesis has become the need
of the day. A number of researchers have addressed the problem of
timing convergence and proposed a variety of solutions ranging from
performing logic synthesis with estimates of physical information to
combining specific sets of synthesis and physical design steps to postponing
synthesis operations to a stage where more accurate physical
information is available. However, there...
364.
Deciding diamp;#64256;erence logic in a Nelson-Oppen combination framework
- Diego Caminha Barbosa de Oliveira
O método de combinação de Nelson-Oppen permite que vários procedimentos de decisão, cada um projetado para uma teoria especíamp;#64257;ca, possam ser combinados para inferir sobre teorias mais abrangentes, através do princípio de propagação de igualdades. Provadores de teorema baseados neste modelo são beneamp;#64257;ciados por sua característica modular e podem evoluir mais facilmente, incrementalmente. Diamp;#64256;erence logic é uma subteoria da aritmética linear. Ela é formada por constraints do tipo x amp;#8722; y amp;#8804; c, onde x e y são variáveis e c é uma constante.Diamp;#64256;erence logic é muito comum em vários problemas, como circuitos digitais, agendamento, sistemas temporais, etc. e se...
365.
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 [19].
2. Like HOL [13] 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.
3. Proofs in TLA rely on basic rules of temporal...
366.
Deontic Logic as Founded on Nonmonotonic Logic
- John F. Horty
this paper, however, that the techniques
of nonmonotonic logic may provide a better theoretical framework---at least for the formalization
of commonsense normative reasoning---than the usual modal treatment. After
reviewing some standard approaches to deontic logic, I focus on two areas in which nonmonotonic
techniques promise improved understanding: reasoning in the presence of conflicting
obligations, and reasoning with conditional obligations.
367.
Representing strategies for the connection calculus in rewriting logic
- Bjarne Holen; Einar Broch Johnsen; Arild Waaler
Abstract. Rewriting logic can be used to prototype systems for automated deduction. In this paper, we illustrate how this approach allows experiments with deduction strategies in a flexible and conceptually satisfying way. This is achieved by exploiting the reflective property of rewriting logic. By specifying a theorem prover in this way one quickly obtains a readable, reliable and reasonably efficient system which can be used both as a platform for tactic experiments and as a basis for an optimized implementation. The approach is illustrated by specifying a calculus for the connection method in rewriting logic which clearly separates rules from...
368.
Representing strategies for the connection calculus in rewriting logic
- Bjarne Holen; Einar Broch Johnsen; Arild Waaler
Abstract. Rewriting logic can be used to prototype systems for automated deduction. In this paper, we illustrate how this approach allows experiments with deduction strategies in a flexible and conceptually satisfying way. This is achieved by exploiting the reflective property of rewriting logic. By specifying a theorem prover in this way one quickly obtains a readable, reliable and reasonably efficient system which can be used both as a platform for tactic experiments and as a basis for an optimized implementation. The approach is illustrated by specifying a calculus for the connection method in rewriting logic which clearly separates rules from...
369.
Strong Normalisation of Cut-Elimination in Classical Logic
- C. Urban; Marseille France; G. M. Bierman
In this paper we present a strongly normalising cut-elimination procedure for classical logic. This procedure adapts Gentzen's standard cut-reductions, but is less restrictive than previous strongly normalising cut-elimination procedures. In comparison, for example, with works by Dragalin and Danos et al., our procedure requires no special annotations on formulae and allows cut-rules to pass over other cut-rules. In order to adapt the notion of symmetric reducibility candidates for proving the strong normalisation property, we introduce a novel term assignment for sequent proofs of classical logic and formalise cut-reductions as term rewriting rules. Keywords: Classical Logic, Cut-Elimination, Strong Normalisation, Symmetric Reducibility...
370.
The Underlying Logic of Hoare Logic
- Yuri Gurevich,Andreas Blass
Formulas of Hoare logic are asserted programs # # # where # is a program
and #, # are assertions. The language of programs varies; in the survey
[Apt 1980], one finds the language of while programs and various extensions
of it. But the assertions are traditionally expressed in first-order logic
(or extensions of it). In that sense, first-order logic is the underlying logic
of Hoare logic. We question the tradition and demonstrate, on the simple
example of while programs, that alternative assertion logics have some advantages.
For some natural assertion logics, the expressivity hypothesis in
Cook's completeness theorem is automatically satisfied.
The readers of this column know Quisani,...
371.
Weakly complete axiomatization of exogenous quantum propositional logic
- Mateus, P.; Sernadas, A.
A weakly complete finitary axiomatization for EQPL (exogenous quantum
propositional logic) is presented. The proof is carried out using a non trivial
extension of the Fagin-Halpern-Megiddo technique together with three Henkin
style completions.
372.
Alternating fixpoint theory for logic programs with priority
- Kewen Wang; Lizhu Zhou; Fangzhen Lin
Abstract. van Gelder's alternating fixpoint theory has proven to be a very useful tool for unifying and characterizing various semantics for logic programs without priority. In this paper we propose an extension of van Gelder's alternating fixpoint theory and show that it can be used as a general semantic framework for logic programs with priority. Specifically, we define three declarative and model-theoretic semantics in this framework for prioritied logic programs: prioritized answer sets, prioritized regular extensions and prioritized well-founded model. We show that all of these semantics are natural generalizations of the corresponding semantics for logic programs without priority. We...
373.
An Algorithm for the Induction of Defeasible Logic Theories From
- Databases Benjamin Johnston; Benjamin Johnston; Guido Governatori
Defeasible logic is a non-monotonic logic with applications in rule-based domains such as law. To ease the development and improve the accuracy of expert systems based on defeasible logic, it is desirable to automatically induce a theory of the logic from a training set of precedent data. Empirical evidence suggests that minimal theories that describe the training set tend to be more faithful representations of reality. We show via transformation from the hitting set problem that this global minimization problem is intractable, belonging to the class of NP optimisation problems. Given the inherent di#- culty of finding the optimal solution,...
374.
LPDA: Another look at Tabulation in Logic Programming
- Eric Villemonte De La Clergerie; Bernard Lang
The Logic Push-Down Automaton (LPDA) is introduced as an abstract operational model for the evaluation of logic programs. The LPDA can be used to describe a significant number of evaluation strategies, ranging from the top-down OLD strategy to bottom-up strategies, with or without prediction. Two types of dynamic programming, i.e. tabular, interpretation are defined, one being more efficient but restricted to a subclass of LPDAs. We propose to evaluate a logic program by first compiling it into a LPDA according to some chosen evaluation strategy, and then applying a tabular interpreter to this LPDA. This approach offers great flexibility and...
375.
The Case for More Digital Logic in Computer Architecture
- Mark Hoffman Department; Mark E. Hoffman
New topics, most notably the World Wide Web, have put considerable pressure on the Computer Science curriculum. Computing Curricula 2001represents a consensus that topics in the core must be reduced to accommodate new topics as they emerge. Unfortunately, digital logic has been reduced to 1/3 its original coverage. We argue that more core coverage should be given to digital logic, and that it should be included in Computer Architecture, not Discrete Systems. Digital logic is fundamental theory necessary for all Computer Science graduates; it provides an indispensable link between theory and practice; and it demonstrates recurring concepts, most notably "levels...
376.
The Refined Extension Principle for Semantics of Dynamic Logic Programming
- Jose Julio Alferes; Federico Banti; Antonio Brogi; Joao Alexandre Leite
Over recent years, various semantics have been proposed for dealing with updates in the setting of logic programs. The availability of di#erent semantics naturally raises the question of which are most adequate to model updates. A systematic approach to face this question is to identify general principles against which such semantics could be evaluated. In this paper we motivate and introduce a new such principle -- the refined extension principle. Such principle is complied with by the stable model semantics for (single) logic programs. It turns out that none of the existing semantics for logic program updates, even though generalisations...
377.
On Warranted Inference in Possibilistic Defeasible Logic Programming
- Carlos Chesñevar; Guillermo Simari; Lluís Godo; Teresa Alsinet
Possibilistic Defeasible Logic Programming (P-DeLP) is a logic programming language which combines features from argumentation theory and logic programming, incorporating as well the treatment of possibilistic uncertainty and fuzzy knowledge at object-language level. Defeasible argumentation in general and P-DeLP in particular provide a way of modelling non-monotonic inference. From a logical viewpoint, capturing defeasible inference relationships for modelling argument and warrant is particularly important, as well as the study of their logical properties. This paper analyzes a non-monotonic operator for P-DeLP which models the expansion of a given program by adding new weighed facts associated with warranted literals. Different logical...
378.
IOS Press Quasi-Possibilistic Logic and its Measures of Information and Conflict
- Didier Dubois; Sébastien Konieczny; Henri Prade
Abstract. Possibilistic logic and quasi-classical logic are two logics that were developed in artificial intelligence for coping with inconsistency in different ways, yet preserving the main features of classical logic. This paper presents a new logic, called quasi-possibilistic logic, that encompasses possibilistic logic and quasi-classical logic, and preserves the merits of both logics. Indeed, it can handle plain conflicts taking place at the same level of certainty (as in quasi-classical logic), and take advantage of the stratification of the knowledge base into certainty layers for introducing gradedness in conflict analysis (as in possibilistic logic). When querying knowledge bases, it may...
379.
Logical control of an elevator with defeasible logic
- Michael A. Covington
tance and encouragement. The elevator control program described in this journal by Dyck and Caines [2] can be implemented more concisely in d-Prolog, a defeasible logic program-ming system developed by Nute [3, 4, 5]. In defeasible logic, more specific rules take precedence over more general ones. Thus, the d-Prolog program-mer can state general rules and then give explicit exceptions, just as humans do when explaining complex regularities to each other.
380.
GDP Festschrift ENTCS, to appear Abstract Nominal Equational Logic
- Ranald A. Clouston; Andrew M. Pitts
This paper studies the notion of “freshness ” that often occurs in the meta-theory of computer science languages involving various kinds of names. Nominal Equational Logic is an extension of ordinary equational logic with assertions about the freshness of names. It is shown to be both sound and complete for the support interpretation of freshness and equality provided by the Gabbay-Pitts nominal sets model of names, binding and α-conversion.
