On Semantics of a Term Calculus for Classical Logic
Silvia Likavec, Pierre Lescanne (2012)
Publications de l'Institut Mathématique
Similarity:
The search session has expired. Please query the service again.
The search session has expired. Please query the service again.
Displaying similar documents to “Sequent Calculus, Derivability, Provability. Gödel's Completeness Theorem”
On Semantics of a Term Calculus for Classical Logic
Corcoran's Aristotelian syllogistic as a subsystem of first-order logic.
Andrade, Edgar J., Becerra, Edward (2007)
Revista Colombiana de Matemáticas
Similarity:
Transition of Consistency and Satisfiability under Language Extensions
Julian J. Schlöder, Peter Koepke (2012)
Formalized Mathematics
Similarity:
This article is the first in a series of two Mizar articles constituting a formal proof of the Gödel Completeness theorem [17] for uncountably large languages. We follow the proof given in [18]. The present article contains the techniques required to expand formal languages. We prove that consistent or satisfiable theories retain these properties under changes to the language they are formulated in.
Strong normalization proofs for cut elimination in Gentzen's sequent calculi
Elias Bittar (1999)
Banach Center Publications
Similarity:
We define an equivalent variant of the Gentzen sequent calculus . In weakenings or contractions can be performed in parallel. This modification allows us to interpret a symmetrical system of mix elimination rules 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.
First Order Languages: Further Syntax and Semantics
Marco Caminati (2011)
Formalized Mathematics
Similarity:
Third of a series of articles laying down the bases for classical first order model theory. Interpretation of a language in a universe set. Evaluation of a term in a universe. Truth evaluation of an atomic formula. Reassigning the value of a symbol in a given interpretation. Syntax and semantics of a non atomic formula are then defined concurrently (this point is explained in [16], 4.2.1). As a consequence, the evaluation of any w.f.f. string and the relation of logical implication are...
Computational Interrpretations of Logics
Silvia Ghilezan, Silvia Likavec (2009)
Zbornik Radova
Similarity:
On the geometry of intuitionistic S4 proofs.
Goubault-Larrecq, Jean, Goubault, Éric (2003)
Homology, Homotopy and Applications
Similarity:
Semantics of MML Query
Grzegorz Bancerek (2012)
Formalized Mathematics
Similarity:
In the paper the semantics of MML Query queries is given. The formalization is done according to [4]
On the categorical semantics of elementary linear logic.
Laurent, Olivier (2009)
Theory and Applications of Categories [electronic only]
Similarity:
The Axiomatization of Propositional Linear Time Temporal Logic
Mariusz Giero (2011)
Formalized Mathematics
Similarity:
The article introduces propositional linear time temporal logic as a formal system. Axioms and rules of derivation are defined. Soundness Theorem and Deduction Theorem are proved [9].
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.