
Authors:
Michael SOLTYS
Title:Extended Frege and Gaussian Elimination
Pages:189205
File:bibtex
Abstract ( + )
We show that the Gaussian Elimination algorithm can be proven correct with uniform Extended Frege proofs of polynomial size, and hence feasibly. More precisely, we give short uniform Extended Frege proofs of the tautologies that express the following: given a matrix A, the Gaussian Elimination algorithm reduces A to rowechelon form. We also show that the consequence of this is that a large class of matrix identities can be proven with short uniform Extended Frege proofs, and hence feasibly.

Authors:
Vladimir V.RYBAKOV
Title:Unification in Common Knowledge Logics
Pages:207215
File:bibtex
Abstract ( + )
his paper alalizes logical unification in Common Knowledge Logics. The unification problem is: for two arbitrary given formulas with metavariables (coefficients) to answer whether they are unifiable in Common Knowledge Logics, and if yes to construct an unifier. We show that the basic common knowledge logic CKL_{n} is decidable w.r.t logical unification of the common knowledge formulas, and that for unifiable common knowledge formulas we can construct an unifier. This result is extended to a wide class of logics expanding CKL_{n}.

Authors:
George WEAVER and Edward THOMPSON
Title:Hermes Algebras
Pages:217229
File:bibtex
Abstract ( + )
For each n>0, an nadic Hermes algebra is a unary algebra of the form B = (B, h_{1}, o, h_{n}) where B is a nonempty set (the domain of B), for each i between 1 and n, h_{i} is an injective unary function on B, and when i and j are different the image of B under h_{i} and the image of B under h_{j} are disjoint. When n = 1, the nadic Hermes algebras are just the Dedekind algebras. For each n, the generalized arithmetics on n characters are nadic Hermes algebras. It is shown that each Hermes algebra can be decomposed into a family of disjoint, countable subalgebras. Members of this family are the configurations of the algebra. When n = 1, there are finite configurations and there are A isomorphism types of configurations. When n > 1, all configurations are infinite and there are 2^{ω} isomorphism types of configurations. Each Hermes algebra is associated with a function (called its configuration signature). The configuration signature counts the number of configurations in each isomorphism type occurring in the decomposition of the algebra. It is shown that two nadic Hermes algebras are isomorphic iff their configuration signatures are identical.

Authors:
Christian J. RENTERIA and Edward Hermann HAEUSLER
Title:A Natural Deduction System for CTL
Pages:231240
File:bibtex
Abstract ( + )
CTL (Computation Tree Logic) is a logic used both for the synthesis and for the verification of concurrent programs. Usually presented in the Hilbert style (axiomatic), it has been adapted for sequent calculus, but without normalization. The aim of the present work is to present a Natural Deduction system for CTL. For that reason the original language has been modified, and labelled formulas have been used. It has been proved that the system is correct and complete. Then the possibility of normalizing the proofs is studied and it is seen, as expected, that strong normalization is achieved in the system without the induction rule.

Authors:
S.P. ODINTSOV
Title:On the embedding of Nelson's logics
Pages:241248
File:bibtex
Abstract ( + )
It will be shown that Nelson's constructive logic with strong negation N3 can be faithfully embedded into its paraconsistent analog N4.