The search session has expired. Please query the service again.

The search session has expired. Please query the service again.

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.