Search

Inspired by the wonderful design and implementation of the Prolog language afforded by the Warren Abstract Machine (WAM), this paper describes an extended logical language which can compute larger realms of first-order logic, based upon theories for finitary geometric logic. The paper describes a Geolog language for expressing first-order geometric logic in tidy closed form, a mathematical Skolem Machine that computes the language, and an implementation prototype that intimately mimics the abstract machine, and which also reformulates expensive bottom-up inference into efficient top-down inference. There are promising mathematical theorem proving applications for geometric logic systems, collected on the website [5]. The emphasis of this paper is theory, abstract machine design and direct implementation of the abstract machine. [ABSTRACT FROM AUTHOR]

Sequence logic is a parameterized logic where the formulas are sequences of formulas of some arbitrary underlying logic. The sequence formulas are interpreted in certain linearly ordered sets of models of the underlying logic. This interpretation induces an entailment relation between sequence formulas which strongly depends on which orderings one wishes to consider. Some important classes are: all linear orderings, all dense linear orderings and all (or some specific) wellorderings. For all these classes one can ask for a sound and complete proof system for the entailment relation, as well as for its decidability. For the class of dense linear orderings and all linear orderings we give sound and complete proof systems which also yield decidability (assuming that the underlying logic is sound, complete and decidable). We formulate some open problems on the entailment relation in the case of wellorderings. [ABSTRACT FROM AUTHOR]

Through a reduction of the halting problem for register machines we prove that it is undecidable whether or not a coherent formula is a logical consequence of a coherent theory. We include a simple completeness proof for coherent logic. Although not published in the present form, these results seem to be folklore. Therefore we do not claim originality. Given the undecidability of the halting problem for register machines the presentation is self-contained. [ABSTRACT FROM AUTHOR]

First-order coherent logic (CL) extends resolution logic in that coherent formulas allow certain existential quantifications. A substantial number of reasoning problems (e.g., in confluence theory, lattice theory and projective geometry) can be formulated directly in CL without any clausification or Skolemization. CL has a natural proof theory, reasoning is constructive and proof objects can easily be obtained. We prove completeness of the proof theory and give a linear translation from FOL to CL that preserves logical equivalence. These properties make CL well-suited for providing automated reasoning support to logical frameworks. The proof theory has been implemented in Prolog, generating proof objects that can be verified directly in the proof assistant Coq. The prototype has been tested on the proof of Hessenberg's Theorem, which could be automated to a considerable extent. Finally, we compare the prototype to some automated theorem provers on selected problems. [ABSTRACT FROM AUTHOR]

A software program requesting a resource that is not available usually raises an out-of-resource exception. Component software is software that has been assembled from standardized, reusable components which, in turn, may also composed from other components. Due to the independent development and reuse of components, component software has a high risk of causing out-of-resource exceptions. We present a small component language and develop a type system which can statically prevent this type of errors . This work continues our previous works [3,18] by including explicit deallocation. We prove that the type system is sound with respect to safe deallocation and that sharp resource bounds can be computed statically. [ABSTRACT FROM AUTHOR]

We provide techniques to integrate resolution logic with equality in type theory. The results may be rendered as follows. A clausification procedure in type theory, equipped with a correctness proof, all encoded using higher-order primitive recursion.A novel representation of clauses in minimal logic such that the λ-representation of resolution proofs is linear in the size of the premisses.A translation of resolution proofs into lambda terms, yielding a verification procedure for those proofs.The power of resolution theorem provers becomes available in interactive proof construction systems based on type theory. [ABSTRACT FROM AUTHOR]

We provide rules for calculating with invariants in process algebra with data, and illustrate these with examples. The new rules turn out to be equivalent to the well known Recursive Specification Principle which states that guarded recursive equations have at most one solution. In the setting with data this is reformulated as ‘every convergent linear process operator has at most one fixed point' (CL-RSP). As a consequence, one can carry out verifications in well-known process algebras satisfying CL-RSP using invariants. [ABSTRACT FROM AUTHOR]