Admissible Substitutions in Sequent Calculi

For first-order classical logic a new notion of admissible substitution is defined. This notion allows optimizing the procedure of the application of quantifier rules when logical inference search is made in sequent calculi. Our objective is to show that such a computer-oriented sequent technique may be created that does not require a preliminary skolemization of initial formulas and that is efficiently comparable with methods exploiting the skolemization. Some results on its soundness and completeness are given.

Operational Calculi for the Euler Operator

2000 Mathematics Subject Classification: 44A40, 44A35

Three-Dimensional Operational Calculi for Nonlocal Evolution Boundary Value Problems

Иван Христов Димовски, Юлиан Цанков Цанков - Построени са директни операционни смятания за функции u(x, y, t), непрекъснати в област от вида D = [0, a] × [0, b] × [0, ∞). Наред с класическата дюамелова конволюция, построението използва и две некласически конволюции за операторите ∂2x и ∂2y. Тези три едномерни конволюции се комбинират в една тримерна конволюция u ∗ v в C(D). Вместо подхода на Я. Микусински, основаващ се на конволюционни частни, се развива алтернативен подход с използване на мултипликаторните частни на конволюционната алгебра (C(D), ∗).