| 1. Michael SOLTYS, Extended Frege and Gaussian Elimination | 189 [Abstract] [PDF] |
| 2. V. V. RYBAKOV, Unification in Common Knowledge Logics | 207 [Abstract] [PDF] |
| 3. George WEAVER and Edward THOMPSON, Hermes Algebras | 217 [Abstract] [PDF] |
| 4. Christian J. RENTERIA and Edward H. HAEUSLER, A Natural Deduction System for CTL | 231 [Abstract] [PDF] |
| 5. S. P. ODINTSOV, On the embedding of Nelson's logics | 241 [Abstract] [PDF] |
1. Michael SOLTYS, Extended Frege and Gaussian
Elimination
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 row-echelon 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.
2. V. V. RYBAKOV, Unification in Common Knowledge Logics
This paper alalizes logical unification in Common Knowledge Logics. The unification
problem is: for two arbitrary given formulas with meta-variables
(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 CKLn 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 CKLn.
3. George WEAVER and Edward THOMPSON, Hermes Algebras
For each n>0, an n-adic Hermes algebra is a unary algebra of the form
B = (B, h1, o, hn) where B is a non-empty set
(the domain of B), for each i between 1 and n, hi is an
injective unary function on B, and when i and j are different the image of B
under hi and the image of B under hj are disjoint. When
n = 1, the n-adic Hermes algebras are just the Dedekind algebras. For each n,
the generalized arithmetics on n characters are n-adic 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 n-adic
Hermes algebras are isomorphic iff their configuration
signatures are identical.
4. Christian J. RENTERIA and Edward H. HAEUSLER, A Natural Deduction
System for CTL
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.
5. S. P. ODINTSOV, On the embedding of Nelson's logics
It will be shown that Nelson's constructive logic with strong negation N3 can
be faithfully embedded into its paraconsistent analog N4.