301.
Logic of Predicates Versus Linear Logic
- Marek A. Bednarczyk
This paper aims at supporting the same idea. Our justification of the claim is, however,
quite different from the one envisaged by Girard. The latter, cf. [11], is proof-theoretic in
nature. Firstly, every sequent of classical, resp., intuitionistic, logic is translated into a sequent
of commutative linear logic with exponentials. Then one shows that the former can be proved
classically, resp., intuitionistically, iff its translation can be proved linearly.
Here it is shown that every theory of classical logic of predicates with equality lives in
a sufficiently rich theory built over a non-commutiative intuitionistic substructural logic: the
logic of predicates with explicit substitution. This perspective does not...
302.
A Logic for Variable Aliasing in Logic Programs
- Elena Marchiori
. This paper introduces a logic for a class of properties - in
particular variable aliasing - used in static analysis of logic programs.
The logic is shown to be sound, complete and decidable. Moreover, it is
illustrated how this logic can be applied to automatize some parts of the
reasoning when proving the partial correctness of a logic program.
1 Introduction
A number of properties of substitutions have been identified as crucial when
analyzing the run-time behaviour of logic programs. They involve groundness
and aliasing: for a substitution ff, a variable x is said to be ground if xff does
not contain variables; x and y are said...
303.
Combining Default Logic and Autoepistemic Logic
- Choh Man Teng
When we work with information from multiple sources, the formats of the knowledge
bases may not be uniform. It would be desirable to be able to combine a knowledge base
of default rules with one containing autoepistemic formulas. Previous works on relating
default logic and autoepistemic logic mostly impose some constraints on autoepistemic
logic, and thus are not suitable for combining the two logics. We first present a fixed
point formulation of autoepistemic logic analogous to that of default logic. Then we
introduce a possible world framework with a partition structure, which corresponds to
our intuitive notion of accessibility as linking alternate "possible" worlds. We show
that both...
304.
Detecting Unsolvable Queries for Definite Logic Programs
- Maurice Bruynooghe; Henk Vandecasteele; D. Andre De Waal; Marc Denecker; Marc
. In solving a query, the SLD proof procedure for definite programs sometimes searches an infinite space for a non existing solution. For example, querying a planner for an unreachable goal state. Such programs motivate the development of methods to prove the absence of a solution. Considering the definite program and the query / Q as clauses of a first order theory, one can apply model generators which search for a finite interpretation in which the program clauses as well as the clause false / Q are true. This paper develops a new approach which exploits the fact that all...
305.
Sequential Logic Optimization with Implicit Retiming and Resynthesis
- S. Bommu; M. Ciesielski; N. O'Neill; P. Kalla
This paper introduces a new logic transformation that integrates retiming with algebraic and Boolean transformations at the technology-independent level. It offers an additional degree of freedom in sequential network optimization resulting from implicit retiming across logic blocks and fanout stems. The application of this transformation to sequential network synthesis results in the optimization of logic across register boundaries. We have implemented our new technique within the SIS framework and demonstrated its effectiveness in terms of cycle-time minimization on a set of sequential benchmark circuits. Keywords Sequential Logic Synthesis, Logic Optimization, Retiming 1 INTRODUCTION Over the years, sequential circuit synthesis has...
306.
Classical vs Non-classical Logics - The Universality of Classical Logic
- Im Stadtwald; Dov M. Gabbay; Dov M Gabbay
This report investigates the question of the universality of classical logic. The approach is to show that an almost arbitrary logical system can be translated reasonably intuitively and almost automatically into classical logic. The path leading to this result goes through the analysis of what is a reasonable logic, how to find semantics for it, how to build a labelled deductive system (LDS) for it, how to translate a LDS into classical logic and how to automate the process using SCAN. This report relies on other papers, published and/or to be published as explained in the acknowledgements. Keywords classical logic,...
307.
VisAll: A new Tool to Visualise Parallel Execution of Logic Programs
- Nuno Fonseca; Vítor Santos Costa; Inês de Castro Dutra; Costa Ines; Castro Dutra
Logic programming allows to explore the full potential of parallelism in the programs in a transparent manner. Several systems were developed to explore the implicit parallelism of logic programs. The development of these systems brings some hard problems such as parallel debugging and dynamic distribution of varied sized work among processors. This paper describes VisAll, a new tool to visualise the parallel execution of logic programs, whose main objective is to help users to develop parallel logic programming systems. VisAll can visualise several kinds of parallelism including or-parallelism, independent and-parallelism, and combinations of both. The system is modular and reasonably...
308.
Applying SLD-Resolution to a Class of Non-Horn Logic Programs
- Grigoris Antoniou; Elmar Langetepe
Methods for dealing with a Horn logic program and one goal are well-known and successful. Here we are concerned with treating logic programs enhanced by some negative literals using the same methods, in particular SLD-resolution. We describe the approach and show its correctness. The result can be applied to default reasoning and has some relevance for model elimination based theorem proving. Keywords: logic programming, default reasoning, model elimination, theorem proving 1 Introduction The problem of checking a goal against a definite logic program has been solved in a satisfactory way a long time ago using SLD-resolution [4]. In this paper...
309.
Semantics of Concurrent Logic Programming as Uniform Proofs
- Paolo Volpe
We describe LC , a formalism based on the proof theory of linear logic, whose aim is to specify concurrent computations and whose language restriction (as compared to other linear logic language) provides a simpler operational model that can lead to a more practical language core. The LC fragment is proveded to be an abstract logic programming language, that is any sequent can be derived by uniform proofs. The resulting class of computations can be viewed in terms of multiset rewriting and is reminiscent of the computations arising in the Chemical Abstract Machine and in the Gamma model. The fragment...
310.
Computation of normal logic programs by fibring neural networks
- Vladimir Komendantsky; Anthony Seda
Abstract. In this paper, we develop a theory of the integration of fibring neural networks (a generalization of conventional neural networks) into model-theoretic semantics for logic programming. We present some ideas and results about the approximate computation by fibring neural networks of semantic immediate consequence operators TP and TP, where TP denotes a generalization of TP relative to a many-valued logic analogous to Kleene’s strong logic. We establish a minimalfixed-point semantics for normal logic programs somewhat analogous to the leastfixed-point semantics for definite logic programs. We argue that the class of logic programs for which the approximation by fibring neural...
311.
Qualitative and Quantitative Reasoning in Hybrid Probabilistic Logic Programs
- Emad Saad
Reasoning with qualitative and quantitative uncertainty is required in some real-world applications [6]. However, current extensions to logic programming with uncertainty support representing and reasoning with either qualitative or quantitative uncertainty. In this paper we extend the language of Hybrid Probabilistic Logic programs [28, 25], originally introduced for reasoning with quantitative uncertainty, to support both qualitative and quantitative uncertainty. We propose to combine disjunctive logic programs [10, 17] with Extended and Normal Hybrid Probabilistic Logic Programs (EHPP [25] and NHPP [28]) in a unified logic programming framework, to allow directly and intuitively to represent and reason in the presence of...
312.
Reasoning about Update Logic
Logical frameworks for analysing the dynamics of information processing abound [4, 5, 8,
10, 12, 14, 20, 22]. Some of these frameworks focus on the dynamics of the interpretation
process, some on the dynamics of the process of drawing inferences, and some do both of
these. Formalisms galore, so it is felt that some conceptual streamlining would pay off.
This paper is part of a larger scale enterprise to pursue the obvious parallel between
information processing and imperative programming. We demonstrate that logical tools from
theoretical computer science are relevant for the logic of information flow. More specifically,
we show that the perspective of Hoare logic [13,...
313.
Logic Engineering in Medicine
- Peter Lucas
The safety-critical nature of the application of knowledge-based systems to the field of medicine, demands the adoption of reliable engineering principles with a solid foundation for their construction. Logical languages with their inherent, precise notions of consistency, soundness and completeness offer such a foundation, thus promoting scrutinous engineering of medical knowledge. Moreover, logic techniques provide a powerful means for getting insight into the structure and meaning of medical knowledge used in medical problem solving. Unfortunately, logic is currently only used on a small scale for building practical medical knowledge-based systems. In this paper, the various approaches proposed in the literature...
314.
Logic engineering in medicine
- Peter Lucas
The safety-critical nature of the application of knowledge-based systems to the field of medicine, demands the adoption of reliable engineering principles with a solid foundation for their construction. Logical languages with their inherent, precise notions of consistency, soundness and completeness offer such a foundation, thus promoting scrutinous engineering of medical knowledge. Moreover, logic techniques provide a powerful means for getting insight into the structure and meaning of medical knowledge used in medical problem solving. Unfortunately, logic is currently only used on a small scale for building practical medical knowledge-based systems. In this paper, the various approaches proposed in the literature...
315.
Stratified coherent spaces: a denotational semantics for Light Linear Logic
- Patrick Baillot; Patrick Baillot; Patrick Baillot
Light linear logic (LLL) was introduced by Girard as a logical system capturing the class of polytime function within the proofs-as-programs approach. This paper deals with the denotational semantics of LLL: we introduce a variant of coherent spaces and prove that it is a sound model for this system, but not for usual linear logic. A simpler version of the model yields a sound semantics of Elementary linear logic, which is the analog of LLL for the class of Kalmar elementary functions.
316.
.2 Classical Logic
Since hypotheses and their restrictions are critical for linear logic, we give here a
formulation of natural deduction for intuitionistic logic with localized hypotheses,
but not parameters. For this we need a notation for hypotheses which we
call a context.
Contexts Gamma ::= Delta j Gamma; u:A
Here, "Delta" represents the empty context, and Gamma; u:A adds hypothesis ` A labelled
u to Gamma. We assume that each label u occurs at most once in a context in order
to avoid ambiguities. The main judgment can then be written as Gamma ` A, where
Delta; u 1 :A 1 ; : : : ; un :An ` A
stands...
317.
.2 Classical Logic
Since hypotheses and their restrictions are critical for linear logic, we give here a
formulation of natural deduction for intuitionistic logic with localized hypotheses,
but not parameters. For this we need a notation for hypotheses which we
call a context.
Contexts Gamma ::= Delta j Gamma; u:A
Here, "Delta" represents the empty context, and Gamma; u:A adds hypothesis ` A labelled
u to Gamma. We assume that each label u occurs at most once in a context in order
to avoid ambiguities. The main judgment can then be written as Gamma ` A, where
Delta; u 1 :A 1 ; : : : ; un :An ` A
stands...
318.
.2 Classical Logic
Since hypotheses and their restrictions are critical for linear logic, we give here a
formulation of natural deduction for intuitionistic logic with localized hypotheses,
but not parameters. For this we need a notation for hypotheses which we
call a context.
Contexts Gamma ::= Delta j Gamma; u:A
Here, "Delta" represents the empty context, and Gamma; u:A adds hypothesis ` A labelled
u to Gamma. We assume that each label u occurs at most once in a context in order
to avoid ambiguities. The main judgment can then be written as Gamma ` A, where
Delta; u 1 :A 1 ; : : : ; un :An ` A
stands...
319.
.2 Classical Logic
Since hypotheses and their restrictions are critical for linear logic, we give here a
formulation of natural deduction for intuitionistic logic with localized hypotheses,
but not parameters. For this we need a notation for hypotheses which we
call a context.
Contexts Gamma ::= Delta j Gamma; u:A
Here, "Delta" represents the empty context, and Gamma; u:A adds hypothesis ` A labelled
u to Gamma. We assume that each label u occurs at most once in a context in order
to avoid ambiguities. The main judgment can then be written as Gamma ` A, where
Delta; u 1 :A 1 ; : : : ; un :An ` A
stands...
320.
.2 Classical Logic
Since hypotheses and their restrictions are critical for linear logic, we give here a
formulation of natural deduction for intuitionistic logic with localized hypotheses,
but not parameters. For this we need a notation for hypotheses which we
call a context.
Contexts Gamma ::= Delta j Gamma; u:A
Here, "Delta" represents the empty context, and Gamma; u:A adds hypothesis ` A labelled
u to Gamma. We assume that each label u occurs at most once in a context in order
to avoid ambiguities. The main judgment can then be written as Gamma ` A, where
Delta; u 1 :A 1 ; : : : ; un :An ` A
stands...
