A generalized setting for fixpoint theory

The mathematical semantics of programming languages is based largely on certain algebraic structures, usually complete lattices or complete partial orders. The usefulness of these structures is based on the existence of fixpoints of functions defined on the structures, and the fact that these classes of structures are closed under such operations as taking cross-products, disjoint unions or function spaces.This paper proposes more general versions of these structures which still retain the above desirable properties. Thus the techniques of mathematical semantics should become applicable in a wider context than heretofore.One important application is given, which in fact motivated the whole development. It is shown that in the generalized setting the existence of unique minimal solutions for recursive definitions of functions are guaranteed without having to resort to informal arguments of any sort.     

Automated deduction by theory resolution

Theory resolution constitutes a set of complete procedures for incorporating theories into a resolution theorem-proving program, thereby making it unnecessary to resolve directly upon axioms of the theory. This can reduce the length of proofs and the size of the search space. Theory resolution effects a beneficial division of labor, improving the performance of the theorem prover and increasing the applicability of the specialized reasoning procedures. Total theory resolution utilizes a decision procedure that is capable of determining unsatisfiability of any set of clauses using predicates in the theory. Partial theory resolution employs a weaker decision procedure that can determine potential unsatisfiability of sets of literals. Applications include the building in of both mathematical and special decision procedures, e.g., for the taxonomic information furnished by a knowledge representation system. Theory resolution is a generalization of numerous previously known resolution refinements. Its power is demonstrated by comparing solutions of Schubert's Steamroller challenge problem with and without building in axioms through theory resolution.This research was supported by the Defense Advanced Research Projects Agency under Contract N00039-84-K-0078 with the Naval Electronic Systems Command and was also made possible in part by a gift from the System Development Foundation. The views and conclusions contained in this document are those of the author and should not be interpreted as representative of the official policies, either expressed or implied, of the Defense Advanced Research Projects Agency or the United States government.     

Abstract deduction and inferential models for type theory

An inferential semantics for full Higher Order Logic (HOL) is proposed. The paper presents a constructive notion of model, that being able to capture relevant computational aspects is particularly suited for the applications of HOL to computer science. The inferential semantics is based on the introduction of new abstract deduction structures (ADS) that express the action of the Comprehension Axiom in a Higher Order Logic proof. The ADS’s allow to define an inferential algebra of higher order potential proof-trees, endowed with two binary operations, the abstraction and the contraction, each consisting of constructive reductions between potential proofs. Typed formulas are interpreted by sequent trees, and the operations between trees correspond to the logical connectives of the interpreted formula. Higher order logic is sound and complete w.r.t. the given inferential semantics.     

Automated deduction in von Neumann-Bernays-Gödel set theory

I present a new clausal version of NGB set theory, and compare my version with that first given by Boyer et al. [4]. A complete set of reductions for Boolean rings is given, derived from those of Hsiang [7]. I list over 400 theorems proved semiautomatically in elementary set theory, and supply the proofs of several of these, including Cantor's theorem. I present a semiautomated proof that the composition of homomorphisms is a homomorphism, thus solving a challenge problem given in [4]. Using the clauses and heuristics presented, there is no apparent obstacle to the semiautomated development of set theory through considerably more difficult theorems.     

Complex object multi-level fixpoint queries

Recent research in extending the standard algebra for nested relations of Thomas and Fischer follows two lines. One is concerned with expressing queries which involve deeply nested information in a flexible way, avoiding the need for explicit restructuring through nesting and unnesting, another deals with extending the expressive power of the nested algebra by providing iteration or recursion constructs, such as fixpoints. These two lines are studied and combined in a natural and general framework.A preliminary version of this article appeared as [23]. The work reported in this article was supported by the IWONL and the NFWO.     

Finite satisfiability for guarded fixpoint logic

The finite satisfiability problem for guarded fixpoint logic is decidable and complete for 2ExpTime (resp. ExpTime for formulas of bounded width).     

Lattice-theoretical fixpoint theorems in morphological image filtering

In mathematical morphology, Matheron has described the complete lattice structure of several classes of increasing (isotone) operators, such as filters. These results can be interpreted in terms of fixpoints of certain types of transformations of the lattice of increasing operators. Moreover, Heijmans and Serra have given conditions for the construction of such operators by convergence of an iteration of increasing operators. We recall some known lattice-theoretical fixpoint ideas originating from Tarski's 1955 paper. A slight elaboration on the underlying methodology leads to the aforementioned results and some others as a consequence of the general theory.     

A Fixpoint Semantics for Stratified Databases

Przmusinski extended the notion of stratified logic programs,developed by Apt,Blair and Walker,and by van Gelder,to stratified databases that allow both negative premises and disjunctive consequents.However,he did not provide a fixpoint theory for such class of databases.On the other hand,although a fixpoint semantics has been developed by Minker and Rajasekar for non-Horn logic programs,it is tantamount to traditional minimal model semantics which is not sufficient to capture the intended meaning of negation in the premises of clauses in stratified databases.In this paper,a fixpoint approach to stratified databases is developed,which corresponds with the perfect model semantics.Moreover,algorithms are proposed for computing the set of perfect models of a stratified database.     

Proof-carrying code from certified abstract interpretation and fixpoint compression

Proof-carrying code (PCC) is a technique for downloading mobile code on a host machine while ensuring that the code adheres to the host's safety policy. We show how certified abstract interpretation can be used to build a PCC architecture where the code producer can produce program certificates automatically. Code consumers use proof checkers derived from certified analysers to check certificates. Proof checkers carry their own correctness proofs and accepting a new proof checker amounts to type checking the checker in Coq. Certificates take the form of strategies for reconstructing a fixpoint and are kept small due to a technique for fixpoint compression. The PCC architecture has been implemented and evaluated experimentally on a byte code language for which we have designed an interval analysis that allows to generate certificates ascertaining that no array-out-of-bounds accesses will occur.     

Hierarchical deduction

This paper describes an hierarchical deduction proof procedure. This procedure proves a theorem by searching for a proof acceptable to an hierarchical deduction structire; those derivations which are irrelevant to this proof are limited by means of a set of completeness-preserving refinements of the basic procedure, such as constraints on framed literals and on common tails, a proper reduction refinement, a global subsumption constraint, and a level subgoal reordering refinement, etc. In addition to this basic algorithm, we will present a partial set of support strategy and a semantically guided hierarchical deduction for the incorporation of semantics and human factors. The paper concludes with proofs concerning the completeness of the basic algorithm and the results of a computer implementation applied to some nontrivial problems.This work was supported in part by NSF grant MCS-8313499.     

Moving selections into linear least fixpoint queries

Efficient least-fixpoint query evaluation is crucial to using logic as the query language for relational databases. The authors present a selection transposition algorithm that allows selections that are conjunctions of the predicates of the form column &thetas; value to be evaluated ahead of the least-fixpoint operator while processing linear recursive queries. It is also shown that the algorithm transposes the strongest possible selection     

A compact fixpoint semantics for term rewriting systems

This work is motivated by the fact that a “compact” semantics for term rewriting systems, which is essential for the development of effective semantics-based program manipulation tools (e.g. automatic program analyzers and debuggers), does not exist. The big-step rewriting semantics that is most commonly considered in functional programming is the set of values/normal forms that the program is able to compute for any input expression. Such a big-step semantics is unnecessarily oversized, as it contains many “semantically useless” elements that can be retrieved from a smaller set of terms. Therefore, in this article, we present a compressed, goal-independent collecting fixpoint semantics that contains the smallest set of terms that are sufficient to describe, by semantic closure, all possible rewritings. We prove soundness and completeness under ascertained conditions. The compactness of the semantics makes it suitable for applications. Actually, our semantics can be finite whereas the big-step semantics is generally not, and even when both semantics are infinite, the fixpoint computation of our semantics produces fewer elements at each step. To support this claim we report several experiments performed with a prototypical implementation.     

Combining assisted and automated deduction

The quest for proved and reliable software goes through theorem provers, which implement proof search. A main trend of these last ten years has been the combination of assisted and automated deduction. Different approaches to this integration are currently studied focussing on efficiency and/or reliability. A promising research direction is to provide formal systems, programming languages and proof environments that support and integrate the two paradigms of computation and deduction. This revised version was published online in June 2006 with corrections to the Cover Date.     

Dynamic interpretation and hoare deduction

In this paper we present a dynamic assignment language which extends the dynamic predicate logic of Groenendijk and Stokhof [1991: 39–100] with assignment and with generalized quantifiers. The use of this dynamic assignment language for natural language analysis, along the lines of o.c. and [Barwise, 1987: 1–29], is demonstrated by examples. We show that our representation language permits us to treat a wide variety of donkey sentences: conditionals with a donkey pronoun in their consequent and quantified sentences with donkey pronouns anywhere in the scope of the quantifier. It is also demonstrated that our account does not suffer from the so-called proportion problem.Discussions about the correctness or incorrectness of proposals for dynamic interpretation of language have been hampered in the past by the difficulty of seeing through the ramifications of the dynamic semantic clauses (phrased in terms of input-output behaviour) in non-trivial cases. To remedy this, we supplement the dynamic semantics of our representation language with an axiom system in the style of Hoare. While the representation languages of barwise and Groenendijk and Stokhof were not axiomatized, the rules we propose form a deduction system for the dynamic assignment language which is proved correct and complete with respect to the semantics.Finally, we define the static meaning of a program of the dynamic assignment language as the weakest condition such that terminates successfully on all states satisfying , and we show that our calculus gives a straightforward method for finding static meanings of the programs of the representation language.     

Model-checking games for fixpoint logics with partial order models

In this paper, we introduce model-checking games that allow local second-order power on sets of independent transitions in the underlying partial order models where the games are played. Since the interleaving semantics of such models is not considered, some problems that may arise when using interleaving representations are avoided and new decidability results for partial order models of concurrency are achieved. The games are shown to be sound and complete, and therefore determined. While in the interleaving case they coincide with the local model-checking games for the μ-calculus, in a partial order setting they verify properties of a number of fixpoint modal logics that can specify, in concurrent systems with partial order semantics, several properties not expressible with the μ-calculus. The games underpin a novel decision procedure for model-checking all temporal properties of a class of infinite and regular event structures, thus improving, in terms of temporal expressive power, previous results in the literature.