Displaying similar documents to “Computational Interrpretations of Logics”

The Derivations of Temporal Logic Formulas

Mariusz Giero (2012)

Formalized Mathematics

Similarity:

This is a preliminary article to prove the completeness theorem of an extension of basic propositional temporal logic. We base it on the proof of completeness for basic propositional temporal logic given in [12]. We introduce n-ary connectives and prove their properties. We derive temporal logic formulas.

Strong normalization proofs for cut elimination in Gentzen's sequent calculi

Elias Bittar (1999)

Banach Center Publications

Similarity:

We define an equivalent variant L K s p of the Gentzen sequent calculus L K . In L K s p weakenings or contractions can be performed in parallel. This modification allows us to interpret a symmetrical system of mix elimination rules L K s p by a finite rewriting system; the termination of this rewriting system can be machine checked. We give also a self-contained strong normalization proof by structural induction. We give another strong normalization proof by a strictly monotone subrecursive interpretation;...

Strong completeness of the Lambek Calculus with respect to Relational Semantics

Szabolcs Mikulás (1993)

Banach Center Publications

Similarity:

In [vB88], Johan van Benthem introduces Relational Semantics (RelSem for short), and states Soundness Theorem for Lambek Calculus (LC) w.r.t. RelSem. After doing this, he writes: "it would be very interesting to have the converse too", i.e., to have Completeness Theorem. The same question is in [vB91, p. 235]. In the following, we state Strong Completeness Theorems for different versions of LC.

Normal forms in partial modal logic

Jan Jaspars (1993)

Banach Center Publications

Similarity:

A "partial" generalization of Fine's definition [Fin] of normal forms in normal minimal modal logic is given. This means quick access to complete axiomatizations and decidability proofs for partial modal logic [Thi].

Beta-reduction as unification

A. Kfoury (1999)

Banach Center Publications

Similarity:

We define a new unification problem, which we call β-unification and which can be used to characterize the β-strong normalization of terms in the λ-calculus. We prove the undecidability of β-unification, its connection with the system of intersection types, and several of its basic properties.