521.
Constructive Logic and the Medvedev Lattice
- Terwijn, Sebastiaan A.
We study the connection between factors of the Medvedev lattice
and constructive logic. The algebraic properties of these factors determine
logics lying in between intuitionistic
propositional logic and the logic of the weak law of the
excluded middle (also known as De Morgan, or Jankov, logic). We discuss the relation between the weak law of the excluded middle and
the algebraic notion of join-reducibility. Finally we discuss autoreducible degrees.
522.
An Authorization Logic with Explicit Time 1
- Henry Deyoung; Deepak Garg; Frank Pfenning
We present an authorization logic that permits reasoning with explicit time. Following a prooftheoretic approach, we study the meta-theory of the logic, including cut elimination. We also demonstrate formal connections to proof-carrying authorization’s existing approach for handling time and comment on the enforceability of our logic in the same framework. Finally, we illustrate the expressiveness of the logic through examples, including those with complex interactions between time, authorization, and mutable state.
523.
A Logic of Probability with Decidable Model Checking*
A predicate logic of probability, close to the logics of probability of Halpern et al., is introduced. Our main result concerns the following model-checking problem: deciding whether a given formula holds on the structure defined by a given finite probabilistic process. We show that this model-checking problem is decidable for a rather large subclass of formulas of a second-order monadic logic of probability. We discuss also the decidability of satisfiability and compare our logic of probability with the probabilistic temporal logic pCTL*.
524.
An Authorization Logic with Explicit Time 1
- Henry Deyoung; Deepak Garg; Frank Pfenning
We present an authorization logic that permits reasoning with explicit time. Following a prooftheoretic approach, we study the meta-theory of the logic, including cut elimination. We also demonstrate formal connections to proof-carrying authorization’s existing approach for handling time and comment on the enforceability of our logic in the same framework. Finally, we illustrate the expressiveness of the logic through examples, including those with complex interactions between time, authorization, and mutable state.
525.
Characterizing Logic Grammars: A Substructural Logic Approach
- James Andrews,Veronica Dahl
this paper. A substructural logic
sequent calculus proof system is given which is shown to be equivalent to
SDGs for parsing problems, in the sense that a string of terminal symbols is
accepted by a grammar if and only if the corresponding sequent is derivable
in the calculus. One calculus is given for each of the two major interpretations
of SDGs; the two calculi differ by only a small restriction in one
rule. Since SDGs encompass other major grammar formalisms, including
DCGs, the calculi serve to characterize those formalisms as well. /
It is the authors' wish that no agency should ever derive military benefit from the publication
of...
526.
Logic Programming With Sets
- Gabriel M. Kuper
this paper is how to extend logic
programming to handle aggregation. We regard such an extension as an essential
prerequisite to extending logic programming to non-1NF databases.
1
527.
Observational Logic, Constructor-Based Logic,
- Michel Bidoit,Rolf Hennicker,Alexander Kurz
Observability and reachability are important concepts for formal software development. While observability
concepts are used to specify the required observable behavior of a program or system, reachability
concepts are used to describe the underlying data in terms of datatype constructors. In this paper we
first reconsider the observational logic institution which provides a logical framework for dealing with
observability. Then we develop in a completely analogous way the constructor-based logic institution
which formalizes a novel treatment of reachability. Both institutions are tailored to capture the semantically
correct realizations of a specification from either the observational or the reachability point of
view. We show that there is a...
528.
Metaprogramming in Logic
- Jonas Barklund
In this review of metaprogramming in logic we pay equal attention to
theoretical and practical issues: the contents range from mathematical
and logical preliminaries to implementation and applications in,
e.g., software engineering and knowledge representation. The area is
one in rapid development but we have emphasized such issues that
are likely to be important for future metaprogramming languages and
methodologies.
1 Introduction
The term `metaprogramming' relates to `programming' as `metalanguage'
relates to `language' and `metalogic' to `logic': programming where the data
represent programs. It should be no surprise that metaprogramming with
logic programming languages takes advantage of many results from metalogic.
In the most general interpretation we would say that `metaprogramming
' refers...
529.
Preference Logic Programming
- Kannan Govindarajan
This research is concerned with the semantics, applications, and implementation of a declarative
language for specifying constraint optimization and relaxation problems. These problems arise in
diverse application areas---document layout, scheduling, parsing, etc. Existing constraint languages
are ill-equipped to express such problems, and provide ad hoc constructs whose semantics is provided
in an unsatisfactory manner. We propose a principled extension of constraint logic programming for
solving these problems. Our proposed paradigm is called preference logic programming, and we have
shown how to formulate constraint optimization problems as well as heuristics for hard combinatorial
problems in this paradigm. We are presently investigating the kinds of constraint relaxation problems
that can...
530.
An expectation-based model for probabilistic temporal logic
- Carroll Morgan; A. K. Mciver
We interpret the modal µ-calculus over a new model [10], to give a temporal logic suitable for systems exhibiting both probabilistic and demonic nondeterminism. The logical formulae are real-valued, and the statements are not limited to properties that hold with probability 1. In achieving that conceptual step, our technical contribution is to determine the correct quantitative generalisation of the Boolean operators: one that allows many of the standard Boolean-based temporal laws to carry over the reals with little or no structural alteration, even for properties that hold with probability strictly between 0 and 1. The generalisation is not obvious, but...
531.
The Logic of Conditional Negation
- Cantwell, John
It is argued that the "inner" negation $\mathord{\sim}$ familiar from 3-valued logic can be interpreted as a form of
"conditional" negation: $\mathord{\sim}$ is read ' $A$ is false if it has a truth value'. It
is argued that this reading squares well with a particular 3-valued
interpretation of a conditional that in the literature has been seen
as a serious candidate for capturing the truth conditions of the
natural language indicative conditional (e.g., "If Jim went to the
party he had a good time"). It is shown that the logic induced by
the semantics shares many familiar properties with classical
negation, but is orthogonal to both intuitionistic and...
532.
Annals of Pure and Applied Logic 134 (2005) 83–93 Finite information logic
- Rohit Parikh A; Jouko Väänänen B
We introduce a generalization of Independence Friendly (IF) logic in which Eloise (the ∃ player) is restricted to a finite amount of information about Abelard’s (∀’s) moves. This logic isshown to be equivalent to a sublogic ∃ ∀ of first-order logic, to have the finite model property, and to be decidable. Moreover, it gives an exponential compression relative to ∃ ∀ logic. © 2004 Elsevier B.V. All rights reserved.
533.
Dynamic logic for belief revision
- Johan Van Benthem
ABSTRACT. We show how belief revision can be treated systematically in the format of dynamicepistemic logic, when operators of conditional belief are added. The core engine consists of definable update rules for changing plausibility relations between worlds, which have been proposed independently in the dynamic-epistemic literature on preference change. Our analysis yields two new types of modal result. First, we obtain complete logics for concrete mechanisms postulates for belief revision can be analyzed by standard modal frame correspondences for model-changing operations.
534.
Logic Programming for Network Management
- Luís Quintano; Gonçalo Marrafa; Joaquim Godinho; Salvador Abreu
Universidade de Évora’s Integrated Information System (SIIUE) aims at representing the entire universe of concepts useful for the management and day-to-day operation of the Organization. It relies on a first-order logic Description Language to define the schema, represent data and computed relations. This representation is used to generate an objectrelational database that is actually used to interface to the system. In this article we describe an application of this framework to issues of network and services planning, configuration and monitoring.
535.
P.Mich.inv. 2906; Logic; SUMM; FRONT
- Unknown
7.2 x 15 cm; broken off on the left and right sides and at the bottom; two vertical breaks; rough surface partly peeling off; Unknown place, province of Egypt; J; Fragment of logic in the Stoic tradition, dealing with the interpretation of conditional phrases of the pattern "Not if the first the second"; published; Pap; 175-185; ZPE 10; Col. I - ends of 7 lines;; Col. II - 20 (including 2 in upper margin); -
536.
P.Mich.inv. 2906; Logic; DET; FRONT
- Unknown
7.2 x 15 cm; broken off on the left and right sides and at the bottom; two vertical breaks; rough surface partly peeling off; Unknown place, province of Egypt; J; Fragment of logic in the Stoic tradition, dealing with the interpretation of conditional phrases of the pattern "Not if the first the second"; published; Pap; 175-185; ZPE 10; Col. I - ends of 7 lines;; Col. II - 20 (including 2 in upper margin); -
537.
P.Mich.inv. 2906; Logic; DET; FRONT
- Unknown
7.2 x 15 cm; broken off on the left and right sides and at the bottom; two vertical breaks; rough surface partly peeling off; Unknown place, province of Egypt; J; Fragment of logic in the Stoic tradition, dealing with the interpretation of conditional phrases of the pattern "Not if the first the second"; published; Pap; 175-185; ZPE 10; Col. I - ends of 7 lines;; Col. II - 20 (including 2 in upper margin); -
538.
Logic Program Based Updates
- Yan Zhang
We investigate two types of logic program based updates: simple fact updates
and program updates. In the simple fact update, a knowledge base is specified as a
set of facts and can be updated by a logic program, while in the program update, a
knowledge base is specified as a logic program and can be updated by another logic
program. The former is usually viewed as a special case of the latter. It is observed
that the conflict resolution is a key issue in these logic program based updates. Our
approach to the logic program based update has the following features: (1) a prioritized
logic programming is...
539.
Coherent Well-founded Annotated Logic Programs
- Carlos Viegas Damásio; Luís Moniz Pereira; Carlos Viegas Dam'asio; Lu'is Moniz Pereira; Terrance Swift
Extended logic programs and annotated logic programs are two important extensions of normal logic programs that allow for a more concise and declarative representation of knowledge. Extended logic programs add explicit negation to the default negation of normal programs in order to distinguish what can be shown to be false from what cannot be proven true. Annotated logic programs generalize the set of truth values over which a program is interpreted by explicitly annotating atoms with elements of a new domain of truth values. In this paper coherent well-founded annotated programs are defined, and shown to generalize both consistent and...
540.
Two paradigms of logical computation in Affine Logic?
- Affine Logic; G. Bellin; A Silvia Baraldini
We propose a notion of symmetric reduction for a system of proofnets for Multiplicative Affine Logic (MAL + MIX) (namely, multiplicative linear logic with unrestricted Weakening and Mix), related to the "cross-cut" reduction in classical logic LK. We prove that such a reduction has the strong normalization and the Church-Rosser properties. On one hand, the usual asymmetric cut elimination procedure in intuitionistic and linear logic is a form of "computation with garbage collection", and the cancellation of irrelevant parts is uniquely determined at any point of the process; such a paradigm can be applied to classical and affine logic through...
