: In this paper, we show how to encode arbitrary enumerable set of numbers given by register machines within limited EPT0L systems and programmed grammars with unconditional transfer. This result has various consequences, e.g. the existence of nonrecursive sets generable by 1lET0L systems or by programmed grammars with unconditional transfer. Moreover, ordered grammars are strictly less powerful than 1lET0L systems.
While type theories such as Nuprl are expressive logics for theorem proving, they present diiculties for designers of term rewriting systems. The two most serious diiculties are: 1) They do not provide a global equality. Instead users rewrite over arbitrary user-deened relations. 2) Each rewrite step must be proved valid. In general, these proofs cannot be recursively generated. We have overcome these diiculties and designed a package for the Nuprl system that works well in practice. Our solution is an extensible set of functions for directing and validating relational inferences. The heart of our package is a set of operators that use a user-supplied lemma database to create new rewrites from old ones. These routines place no restrictions on relations; a rewrite's success depends on the strength of the database. Overall, the package allows rewrites to be pieced together in numerous ways, providing the user with a tool to construct sophisticated rewrite strategies.
Diierent kinds of logical calculi have diierent advantages and disadvantages. So calculi with a large number of derivation rules have a large scope for searching proofs, but in most cases it is possible to nd short proofs. It should be useful to translate the structures created during the proof in one system into structures of another system in order to examine attributes of proofs in these systems. An algorithm for the optimization of tableau-proofs with respect to the number of nodes is given. It is shown how tableau-structures (not only proofs!) can be translated into resolution-structures. This translation leads to an improvement of the given algorithm for optimization.
Proofs in standard logical calculi have a simple structure (mostly a sequence, tree or set of related formulas). Therefore, formal proofs are hard to understand or to present in an intelligible way. The Block Calculus for rst order logic introduced in this paper is a variant of natural deduction that has highly structured proofs. These proofs can be presented in many ways by hiding blocks of subproofs. Moreover it can be easily extended by other calculi. We characterize the semantics of incomplete proof structures in the Block Calculus and prove it's soundness and completeness.
The MAXGAP problem of a linear integer optimization problem P consists in determining the maximum diierence (gap) (P) between the optimal value z (E) of an instance E 2 P and the LP bound z c (E) with respect to all E 2 P. In the case of the one-dimensional cutting stock problem (1D CSP) it is known that (1D CSP) 1 + 5 132 but there is also a conjecture that (1D CSP) 2. In this paper we show that in the case of the restricted exact 2-stage two-dimensional cutting stock problem (RE2 CSP) the maximum gap increases at least linearly in the number m of pieces. It holds (RE2 CSP) > m 3. For the (non-restricted) exact 2-stage two-dimensional cutting stock problem (E2 CSP) an example is given such that (E2 CSP) 2(1 + 5 132) > 2:075 follows which yields also a lower bound for the general two-dimensional cutting stock problem. Furthermore some consequences for higher-dimensional cutting stock problems and with respect to applications are discussed.
A new data structure, "segmented winner tree", is introduced. This is useful when one needs to represent data that are partitioned into segments. The segment operations that are efficiently supported are: initialize a unit length segment, find the element with least value in any given segment, update an element in any segment, merge two adjacent segments, and split a segment.
In this article we formally describe a declarative approach for encoding plan operatorsin proof planning, the so-called methods. The notion of method evolves from the much studiedconcept tactic and was first used by Bundy. While significant deductive power has been achievedwith the planning approach towards automated deduction, the procedural character of the tacticpart of methods, however, hinders mechanical modification. Although the strength of a proofplanning system largely depends on powerful general procedures which solve a large class ofproblems, mechanical or even automated modification of methods is nevertheless necessary forat least two reasons. Firstly methods designed for a specific type of problem will never begeneral enough. For instance, it is very difficult to encode a general method which solves allproblems a human mathematician might intuitively consider as a case of homomorphy. Secondlythe cognitive ability of adapting existing methods to suit novel situations is a fundamentalpart of human mathematical competence. We believe it is extremely valuable to accountcomputationally for this kind of reasoning.The main part of this article is devoted to a declarative language for encoding methods,composed of a tactic and a specification. The major feature of our approach is that the tacticpart of a method is split into a declarative and a procedural part in order to enable a tractableadaption of methods. The applicability of a method in a planning situation is formulatedin the specification, essentially consisting of an object level formula schema and a meta-levelformula of a declarative constraint language. After setting up our general framework, wemainly concentrate on this constraint language. Furthermore we illustrate how our methodscan be used in a Strips-like planning framework. Finally we briefly illustrate the mechanicalmodification of declaratively encoded methods by so-called meta-methods.
We survey 25 years of research on decidability issues for Petri nets. We collect results on the decidability of important properties, equivalence notions, and temporal logics.
Oriented graphs in which every pair of vertices can be connected by a unique path of given length (not depending on the choice of the pair of vertices) are studied. These graphs are a natural extension of the well-known de Bruijn graphs and retain their most important properties. Some results on the structure of and methods for constructing such graphs are obtained.
