Computer Science Logic

Frontmatter

Monadic second order logic, tree automata and forbidden minors

Abstract

N.Robertson and P.D.Seymour proved that each minor closed class K of graphs is characterized by finitely many minimal forbidden minors. If these minors are given then they can be used to find an efficient membership test for such classes (see [Rob Sey 86b]). From these minors one can get a monadic second order description of the class K. Main result of the article is that from a monadic second order description of the class K. Main result of the article is that from a monadic second order description of K the minimal forbidden minors can be constructed, when K contains only graphs of universally bounded tree width. The result is applied to the class of partial 2-pathes.

Stefan Arnborg, Andrzej Proskurowski, Detlef Seese

On the reduction theory for average case complexity

Abstract

This is an attempt to simplify and justify the notions of deterministic and randomized reductions, an attempt to derive these notions from (more or less) first principles.

Andreas Blass, Yuri Gurevich

From prolog algebras towards WAM-A mathematical study of implementation

Abstract

This is the first part of a work presenting a natural and transparent albeit entirely mathematical description of Warren's 1983 abstract machine for executing Prolog. We derive the description from Börger's 1990b phenomenological description of the language, refining Prolog algebras stepwise, proving conservation of correctness at each step.

Egon Börger, Dean Rosenzweig

A formal operational semantics for languages of type Prolog III

Abstract

We use dynamic algebras introduced by Gurevich in [Gurevich 1988], [Gurevich 1991] to develop a formal semantics for the logical core of constraint logic programming languages of type Prolog III [Colmerauer 1990]. Our specification abstracts away from any particular feature of the mechanism for the resolution of constraints, thus providing a uniform description of constraint logic programming languages which turns out to be a natural refinement of the standard Prolog algebras developed in [Börger 1990]. In particular we show how our method can be used for a precise but simple method to handle specification problems connected to the freeze predicate.

E. Börger, Peter H. Schmitt

Efficiency considerations on goal-directed forward chaining for logic programs

Abstract

This paper presents a linear resolution strategy (GDFC-resolution) for definite logic programs in which goal-directed forward chaining is used to find refutations. GDFC-resolution focuses on relevant facts and rules by means of query independent link clauses. One problem is, that the number of link clauses may be infinite if the program contains recursive rules defined over recursive data structures. We present an approach to generate a more general but finite set of link clauses. We show that GDFC-resolution is sound and complete for definite programs. We discuss the efficiency of GDFC-resolution comparing it with SLD-resolution and present some experimental results.

Wolfram Burgard

Decision problems for tarski and presburger arithmetics extended with sets

D. Cantone, V. Cutello, J. T. Schwartz

A fast garbage collection algorithm for WAM — based PROLOG

Abstract

Garbage collection for Warren abstract machine is complicated by:

• •three semantically distinct types of pointers, whose types must be preserved as well as their relative positions;
• •need for marking used atomic values because of TRAIL compactification;
• •capability of structures to grow incrementally, i.e. in the wrong direction.

Prolog data graphs (DAGs, circular structures would interrput the present algorithm) are represented as linear structures by an invertible pointer reversing transform. Reversal of forward pointers is delayed till needed, so that the algorithm can manage with one pass through the workspace. The technique of delayed reversal enables compactification of (two or more) physically separated memory areas which point at each other.

If the workspace contains n used words k of which are active, the complexity of the algorithm is #x03B1; n + β k + OVERHEAD, where OVERHEAD depends on the structure of active data graphs involved.

Igor Đurđanović

A resolution variant deciding some classes of clause sets

Abstract

In this paper we investigated a special resolution variant, based on an A-ordering, which decides some classes of clause sets. We think that similiar mechanisms may be defined to provide decision algorithms for other interesting classes of clause sets. We shall inquire along this line of arguments into extensions of the Maslov class (i.e. the class of formulas with prefix of type ∀*∃* and at most two literals in each disjunct) in a forthcoming paper.

Christian Fermüller

Subclasses of quantified boolean formulas

Abstract

Using the results of a former paper of two of the authors [KaKB 90], for certain subclasses of quantified Boolean formulas it is shown, that the evaluation problems for these classes are coNP-complete. These subclasses can be seen as extensions of Horn and 2-CNF formulas.

Further it is shown that the evaluation problem for quantified CNF formulas remains PSPACE-complete, even if at most one universal variable is allowed in each clause.

Andreas Flögel, Marek Karpinski, Hans Kleine Büning

Algorithmic proof with diminishing resources part 1

Abstract

We present goal directed computation prcedures for classical, intuitionistic and linear implication. The procedure allows for using assumptions at most once. Completeness is proved and proof theoretic results such as interpolation are indicated

DM Gabbay

Cutting plane versus frege proof systems

Abstract

The cutting plane proof system for proving the unsatisfiability of propositional formulas in conjunctive normalform is based on a natural representation of formulas as systems of integer inequalities. We show: Frege proof systems p-simulate the cutting plane proof system. This strengthens a result in [5], that extended Frege proof systems (which are believed to be stronger than Frege proof systems) p-simulate the cutting plane proof system. Our proof is based on the techniques introduced in [2].

Andreas Goerdt

RAM with compact memory: a realistic and robust model of computation

Abstract

An operation op of arity k on ℕ, i.e. a function op: ℕ^k → ℕ is linear time Turing computable (for short, LTTC) if it is computable in linear time on a Turing machine (for usual binary or dyadic notation of integers). Let + and Conc respectively denote usual addition of integers and concatenation (of their dyadic notations). A RAM which uses only arithmetical operations of a set I is called an I - RAM. An LTTC-RAM is a RAM which only uses LTTC operations.

In the present paper, we use the logarithmic criterion for time measure of RAMs. A RAM works with polynomially (resp. strongly polynomially) compact memory if it only uses addresses (resp. addresses and register contents) ≤ t^O(1) where t is the time of the computation.

Theorem 1. A deterministic LTTC-RAM R with polynomially compact memory is simulated in linear time by a deterministic {+}-RAM (resp. {Conc}-RAM) R' with strongly polynomially compact memory.

Theorem 2. A nondeterministic LTTC-RAM R can be simulated in linear time by a nondeterministic {+}-RAM (resp. {Conc}-RAM) R' with strongly poynomially compact memory.

Note that Theorem 2 holds for both weak nondeterministic RAMs and strong nondeterministic RAMs, i.e. in case the RAMs have only nondeterministic goto instructions or in case they have an instruction to guess an integer.

If moreover the RAMs R of Theorem 1–2 are sane (i.e. R does not use noninitialised registers) then the simulating RAMs R' are sane, too.

We also study and discuss more restrictive notions of compact memory (linearly compact memory).

Etienne Grandjean, J. M. Robson

Randomness and turing reducibility restraints

Abstract

A definition of random sequences equivalent to the one of Martin-Löf and Schnorr motivated by the hierarchy of Turing reducibility restraints is introduced and compared with different similarily obtained notions.

Karol Habart

Towards an efficient tableau proof procedure for multiple-valued logics

Abstract

One of the obstacles against the use of tableau-based theorem provers for non-standard logics is the inefficiency of tableau systems in practical applications, though they are highly intuitive and extremely flexible from a proof theoretical point of view. We present a method for increasing the efficiency of tableau systems in the case of multiple-valued logics by introducing a generalized notion of signed formulas and give sound and complete tableau systems for arbitrary propositional finite-valued logics.

Reiner Hähnle

Interactive proof systems: Provers, rounds, and error bounds

Abstract

We introduce generalized multi-prover interactive proof systems and the associated polynomial time complexity classes IP(m, r, 1/h), which depend on the number m of provers, number r of rounds and the value 1/h by which the error is bounded away from one half. In this denotation the class IP(m, r) of languages accepted by ordinary IP-systems with m provers and r rounds appears as IP(m, r, 1/6), whereas we define IP'(m, r) to be the union of all IP(m, r, 1/h) with an arbitrary polynomial h. We prove several simulation theorems that enable us to prove most of the known relations between different IP-classes and a collapse of the IP' hierarchy to essentially only four classes, namely

$$\begin{gathered}IP'(1,1) = IP(1,1) \subseteq IP'(1,poly) = IP(1,poly) = PSPACE \hfill \\\subseteq IP'(2,1) = IP(poly,1) \hfill \\\subseteq IP'(2,2) = IP(poly,poly) = NEXPTIME \hfill \\\end{gathered}$$

Finally we show how to reduce the space needed by an interactive proof system introducing one additional prover.

Ulrich Hertrampf, Klaus Wagner

Logics for belief dependence

Abstract

In this paper, we investigate the theoretical foundations of belief dependence in multiple agent environment, where agents may rely on someone else about their beliefs or knowledge. Several logics for belief dependence are introduced and studied. First of all, we try to formalize the problem of belief dependence in the framework of general epistemic logics, by which we will argue that general epistemic logic is not appropriate to formalize the problem of belief dependence. Then, based on an approach which is similar to Fagin and Halpern's general awareness logic, we present the second logic for belief dependence, which is called a syntactic approach. The third logic is an adapted possible world logic, where sub-beliefs are directly introduced in the models.

Zhisheng Huang

A generalization of stability and its application to circumscription of positive introspective knowledge

Jan Jaspars

The complexity of adaptive error-correcting codes

Daniele Mundici

Ramsey's theorem in bounded arithmetic

Abstract

We shall show that the finite Ramsey theorem as a Δ₀ schema is provable in IΔ ₀+Ω₁. As a consequence we get that propositional formulas expressing the finite Ramsey theorem have polynomial-size bounded-depth Frege proofs.

Pavel Pudlák

Nontrivial lower bounds for some NP-problems on directed graphs

Abstract

NP-complete problems are believed to be not in P. But only a very few NP-complete problems, and none concerning graph theory, are proved to have a nontrivial time lower bound (i.e. not to be solvable in linear time on a DTM (i.e. deterministic Turing machine). A problem L ε NP is linearly NP-complete if any problem in Ntime (n) can be reduced to it in linear time on a DTM. It follows from the separation result between deterministic and nondeterministic linear-time complexity classes [PPST83], that a linearly NP-complete problem has a nontrivial time lower bound. We present in this paper the first natural problems on graphs which are linearly NP-complete.

Solomampionona Ranaivoson

Expansions and models of autoepistemic theories

Abstract

Autoepistemic logic is a logic for modelling the beliefs of an agent who reflects on his own beliefs. In the paper we discuss problems dealing with existence of autoepistemic models and autoepistemic expansions. The necessary and sufficient conditions for existence of autoepistemic models and expansions are formulated.

Cecylia M. Rauszer

On the existence of fixpoints in moore's autoepistemic logic and the non-monotonic logic of McDermott and Doyle

Abstract

In [6] Moore has introduced a logic to represent the beliefs of ideal rational agents, called autoepistemic logic. This logic was presented as an improvement of the non-monotonic logic of McDermott and Doyle in [4]. We give a new method to characterize the fixpoints in both logics and thus obtain decision procedures for several problems in this context. Although the two logics are conceptually very different our method is very uniform.

Robert F. Stärk

On the tracking of loops in automated deductions

M. E. Szabo

The gap-language-technique revisited

Abstract

Generalizing work of Schöning and others concerning gap language constructs recognizable in polynomial time we examine structural properties of reducibilities defined for various “lower” or “parallel” complexity classes. Finally we show how the proof techniques for the above can be used to show the existence of easy complexity cores for sets which cannot be decided in logarithmic space.

Heribert Vollmer

Backmatter