Добро пожаловать!

Pages:     | 1 |   ...   | 26 | 27 || 29 |

E-mail:V.Rybakov@mmu.ac.uk Мальцевские чтения 2009 Неклассические логики и теория доказательств Decidability of logic N* S. A. Drobyshevich Logic N* is an extension of logic N, suggested by Dosen [1] to study negations weaker then that of Johansson’s minimal logic. N is defined in the language L := {,,, ¬}, where is an intuitionistic implication and ¬ is interpreted as a modal operator of impossibility.

The axiom schemata contains the axioms of positive logic together with the axiom ¬p ¬q ¬(p q) The rules of inference are modus ponens and the contraposition rule for negation.

Definition. W = W,, R, is an N-frame if: (i) W is a non-empty set; (ii) is a partial ordering on W; (iii) R W is an accessibility relation for negation verifying R R.

An N-model is an N-frame together with a valuation satisfying the intuitionistic heredity.

Logic N* was first suggested as a logical framework for investigation of well founded semantics [2] and it is obtained from N by adding the following axioms:

¬(p p) q ¬(p q) ¬p ¬q New axioms allow to define Routley style semantics for N*. Routley frame is W = W,, where W, are defined as above and is anti-monotonic function on W. Routley model is a Routley frame together with a valuation as for N-models. The new definition for negation is x ¬ x Logic N* is complete with respect to the class of Routley frames. Using Routley style semantics we then prove Theorem. Logic N* has a finite model property.

We obtain this result by constructing a hybrid tableau calculus based on the tableau calculus suggested in [3]. From this theorem we infer in a standard way Corollary. Logic N* is decidable.

This work was supported by Russian Foundation for Basic Research, project RFBR-0901-00090-a.

References [1] Dosen K. Negation as a modal operator. Reports on Mathematical Logic, 20 (1986), 15–28.

[2] Cabalar P., Odintsov S. P., Pearce D. Logical Foundations of Well-Founded Semantics. In: P. Doherty et al. (eds.) Principles of Knowledge Representation and Reasoning: Proceedings of the 10th International Conference (KR2006), AAAI Press, Menlo Park, California, 2006, 25–36.

[3] Odintsov S. P., Wansing H. Inconsistency-tolerant description logic. Part II: A tableau algorithm for CALCc. Journal of Applied Logic 6 (2008), 343–360.

Novosibirsk State University, Novosibirsk (Russia) E-mail:2searcher@inbox.ru Мальцевские чтения 2009 Неклассические логики и теория доказательств Comparison of complexities of logical inferences in Hilbert-type system with complexities of inferences in Martin—Lf’s theory of small types G. Marikyan In [1] and [2] Per Martin-Lf has introduced his Intuitionistic Type Theory (hereafter MLTT). To characterize a theory it is important to evaluate complexity of its logical inferences. For this purpose I compare complexity of inferences in a well-known formal system with complexity of inferences in Martin-Lf’s Theory of Small Types [2] (hereafter MLTT0).

For comparison I have chosen the Hilbert-type system (hereafter H) defined in [3]. Both H and MLTT0 are formalizations of arithmetic, that is why it is an interesting problem to compare the complexity of logical inferences in these two formal systems.

In order to compare complexities of inferences I build three methods of complexity measurements universal for both systems, and I use them to compare the complexities of logical inferences in them.

L-complexity of an inference is the number of axioms and rules of inference in it.

D-complexity of an inference in MLTT0 is the total number of symbols of all assumptions and expressions in the inference, plus number of separating symbol “;” in it.

D1-complexity of an inference in H and in MLTT0 is the total number of symbols of all expressions in the inference, plus the number of separating symbol “;” in it.

H,MLT Theorem. SL T0(n) 10n.

H,MLT Theorem. SD T0(n) 28n.

MLTT0,H Theorem. SD (n) > 4n.

MLTT0,H Theorem. SL (n) > 5n.

References [1] Martin-Lf P. Constructive mathematics and computer programming. Sixth International Congress for Logic, Methodology, and Philosophy of Science. Amsterdam: North–Holland, 1982, 153–175.

[2] Martin-Lf P. An Intuitionistic Theory of Types: Predicative Part. Logic Colloquium ’73, H. E. Rose and J. C. Shepherdson. Amsterdam: North–Holland, 1973, 73–118.

[3] Kleene S. C. Mathematical Logic. New York: John Wiley and Sons, Inc, 1967.

State University of New York Empire State College, New York (U.S.A.) E-mail:Gohar.Marikyan@esc.edu Мальцевские чтения 2009 Неклассические логики и теория доказательств On Topological Presentation of Nelson Lattices S. P. Odintsov Priestley duality for N3-lattices modelling explosive Nelson’s logic N3 was developed independently by R. Signoli [1] and A. Sendlewski [4]. The algebraic semantics for paraconsistent Nelson’s logic was only recently developed by the author of this abstract, see [3].

This allows to pose a question on Priestley duality for algebraic models of paraconsistent Nelson’s logic. Here we suggest a Priestley duality for -lattices [3] modelling a version of paraconsistent Nelson’s logic with additional intuitionistic negation, i.e. we construct a category of ordered topological spaces dually equivalent to the category.texNELS of -lattices and their homomorphisms.

Let X = (X, X1,,, g) be a tuple, where X is a set, X1 X, a partial order on X, g : X X, and is a topology on X. Put X2 := g(X1), X+ := {x X | x g(x)}, X- := {x X | g(x) x}.

The structure X is said to be a Nelson space if the following conditions are satisfied:

(1) (X,,, g) is a De Morgan space, i.e., (X,, ) is a Priestley space [2] and g is an order-reversing homeomorphism such that g2 = idX;

(2) X1 is closed in, X = X1 X2, and X1 X2 = X+ X-;

(3) (X1, X1, X1) is a Heyting space, i.e., (U] ={y | y x for some x U} is open for any set U open in X1;

(4) for any x X1 and y X2, if x y, then x X+, y X-, and there exists z X such that x, g(y) z g(x), y;

(5) for any x X2 and x X1, if x y, then x X+, y X-, and x g(y).

For Nelson spaces X = (X, X1,,, g) andY=(Y, Y,,, g ), a mapping f : X Y is said to be a Nelson function if 1) f : (X,, g) (Y,,, g ) is a De Morgan function, i.e., an order preserving continuous mapping such that f g = g f; 2) f(X1) Y ; 3) f X 1 is a Heyting function, i.e., for any U open in, f-1((U Y ]) X1 =(f-1(U Y )] X1.

Denote by NELS the category of Nelson spaces and Nelson functions.

Theorem. The categories NELS and NELS are dually equivalent.

This work was supported by Russian Foundation for Basic Research, project RFBR-0901-00090-a.

References [1] Cignoli R. The class of Kleene algebras satisfying interpolation preperty and Nelson algebras. Algebra Universalis 23, 1986, 262–292.

[2] Davey B., Priestley H. Introduction to Lattices and Order, Cambridge University Press, Cambridge, 2002.

[3] Odintsov S. P. Constructive Negations and Paraconsistency, Springer, Dordrecht, 2008.

[4] Sendlewski A. Nelson algebras through Heyting ones. Studia Logica 49, 1990, 106-126.

Sobolev Institute of Mathematics, Novosibirsk E-mail:odintsov@math.nsc.ru Мальцевские чтения 2009 Неклассические логики и теория доказательств Tableau-like automata-based axiomatization for fix-point propositional modal calculus N. V. Shilov We develop sound and complete experimental tableau-like axiomatization for the propositional µ-Calculus of D. Kozen (µC) [1]. This axiomatization is automata decision procedure augmented by model checking deciding automata as a finite model. A deduction strategy within the axiomatization consists of a number of stages. These stages are sketched below along with outlines of the approach.

First we introduce the rewriting rules that eliminate negations outside literals. The rules preserve tautologies and lead to a so-called simple formulae. Then we study a special class of automata on infinite words. An automaton in this class accepts an infinite word as soon as it enters any accepting control state. A (fairness) constraint is a set of input symbols. An infinite word meets the constraint iff all specified symbols occur finite number of times at most. The halting (termination) problem with the constraint consists in checking whether an automaton accepts all infinite words that meet the constraint (if it is the case than we say that the automaton totally accept the constraint). We prove that the problem is decidable. We do believe that automata-theoretic approach to decidability can exploit different variants of automata, not necessary well-known (i.e. Bchi or Rabin) automata.

At the next step we translate simple formulae of µC into automata with fairness constraint. Control states of the automata are finite sets of formulae. The main property of this translation follows: a formula is a tautology iff the automaton totally accepts the constraint. After that we consider automata as finite labeled transition systems (i.e. Kripke structures) for µC, and encode the halting problem with constrains by a particular formula of µC. An automaton totally accepts a constraint iff the formula holds in some initial state of the corresponding model. In simple words: we interpret halting problem with fairness constraint as the local model checking problem for some fixed formula of the propositional µ-Calculus.

Finally we adopt sound and complete tableau designed for local model checking for the µC in finite models [2] and convert it into a tableau-like axiomatization for the propositional µ-Calculus of D. Kozen.

References [1] Kozen D. Results on the Propositional Mu-Calculus. Theoretical Computer Science, 27 (1983), 333–354.

[2] Cleaveland R. Tableau-based model checking in the propositional mu-calculus. Acta Informatica, 27(1990), 725–747.

A. P. Ershov Institute of Informatics Systems, Novosibirsk, Russia E-mail:shilov@iis.nsk.su IX. Секция «Логические аспекты программирования» Мальцевские чтения 2009 Логические аспекты программирования Вычислимая логическая спецификация параллельных систем В. Н. Глушкова Семантика асинхронных параллельных программ представляется логической спецификацией из 0-формул [1] с ограниченными кванторами всеобщности. Формулы интерпретируются на дереве разбора программы, представленном списком, структуру которого отражает префикс формулы вида (x1r1)...(xnrn), — транзитивное замыкание отношения принадлежности списку. Для построения модели используются квазитождества ( ( где () конъюнкция атомных формул или их отрицаx) x), ний вида p, 1 = 2 (f = ) ; p, f — предикатный и функциональный символы, 1, 2 — термы.

Спецификация описывает поведение системы через изменение состояний ее переменных. Выделяются многосортные области интерпретации: Var — переменные, Ps – множество всех процессов, Op — операторы и т.д. Для описания последовательности исполнения операторов явно используется переменная сорта “дискретное время”; функция Val : Ps Var N D задает значения переменных процесса в момент времени n в области D. Время является общим для всех процессов программы, а при интерпретации формул изменяется на 1 только одним процессом, поэтому для корректности определения функции и предикаты позитивно продолжаются по n. Для программ с конечным числом состояний можно построить модель Крипке M = (S, S0, R.L), S, S0 — множества всех и начальных состояний; R S S — отношение переходов;

L : S 2AP — функция, задающая для каждого состояния множество истинных атомных формул. Эта модель представляется графом, количество ”входных” вершин которого равно числу альтернативных начальных значений переменных. Узлы графа содержат помимо значений переменных метки активных операторов. Интерпретатор генерирует граф при реализации правила вывода ”modus ponens”. Из каждой вершины выходит число дуг равное количеству процессов. Дуги соответствуют переходу от времени n к n +1. Новая вершина генерируется только в том случае, если при переходе получены новые значения переменных и меток активных операторов; иначе дуга проводится к старому узлу графа, содержащему эти значения. После завершения построения графа просмотром всех его вершин легко проверить свойство взаимного исключения, чтобы убедиться в корректном использовании разделяемых ресурсов.

Список литературы [1] Goncharov S.S., Sviridenko D.I. Theoretical aspects of -programming. Mathematical Methods of Specification and Synthesis of Software Systems’ 85. Proc. of the Internat. Spring School. Springer-Verlag, April, 1985.

ДГТУ, Ростов-на-Дону E-mail:lar@rsu.ru; lar@aaanet.ru Мальцевские чтения 2009 Логические аспекты программирования О графах существенной зависимости правильных семейств функций В. А. Носов, А. Е. Панкратьев Семейство булевых функций F = {fi}n, fi = fi(z1,..., zn), называется праi= вильным [1], если для произвольных несовпадающих наборов z = (z1, z2,..., zn) и z =(z1, z2,..., zn) найдётся индекс 1, n такой, что z = z и f(z1,..., zn) =f(z1,..., zn).

Напомним, что графом существенной зависимости [3] семейства функций F = {fi}n, fi = fi(z1,..., zn), называется ориентированный граф GF =(V, E) на множеi=стве вершин V = {1, 2,..., n} такой, что (i, j) E если и только если функция fj существенно зависит от xi.

Пусть C — ориентированный цикл в орграфе G(V, E). Стягиванием цикла C C назовём операцию перехода от графа G(V, E) к графу GC(V, EC), полученному удалением из графа G(V, E) всех рёбер, входящих в цикл C, и отождествлением всех вершин, входящих в цикл C.

Теорема. Пусть конечный ориентированный граф G(V, E) без петель и кратных рёбер является правильным (реализуется в виде графа существенной зависимости некоторого правильного семейства функций). Тогда для любого простого неукорачиваемого цикла C G граф GC, полученный стягиванием цикла C, содержит кратные ребра.

Теорема. Пусть G(V, E) — произвольный ориентированный граф без петель и кратных ребер на n вершинах V = {1, 2,..., n}.

Тогда существует правильный граф G (V, E ) на n n + log2 n вершинах V = {1, 2,..., n }, такой, что его вершинный подграф на подмножестве V V совпадает с G.

При этом для любого семейства функций F = {fi}n, реализующего исходный i= граф G, найдётся правильное семейство функций F = {fi }n, реализующее граф G i=и такое, что для каждого i, 1 i n, существует набор значений аргументов xn+1,..., xn, при которых fi как функция от n аргументов x1,..., xn совпадает с fi.

Список литературы [1] Носов В. А. Критерий регулярности булевского неавтономного автомата с разделённым входом.

Интеллектуальные системы, 3 (1998), вып. 3–4, с. 269–280.

[2] Носов В. А., Панкратьев А. Е. Латинские квадраты над абелевыми группами. Фундаментальная и прикладная математика, 12 (2006), вып. 3, с. 65–71.

[3] Носов В. А., Панкратьев А. Е. О семействах функций, задающих латинские квадраты над абелевыми группами. Вестник Московского государственного университета леса — Лесной вестник, 2(51) (2007), с. 141–144.

Московский государственный университет имени М. В. Ломоносова, Москва E-mail:vnosov40@mail.ru; anton.pankratiev@gmail.com Мальцевские чтения 2009 Логические аспекты программирования On varieties generated by algebras of relations D. A. Bredikhin A set of binary relations closed with respect to some collections of operations forms an algebra which is called an algebra of relations. Any algebra of relations can be considered as partial ordered by set-theoretical inclusion. Tarski was the first to treat algebras of relations from the point of view of universal algebra. Now, the theory of algebras of relations is an essential part of modern algebraic logic.

We shall concentrate our attention on the operations of relation product, union, and two unary operations, defined as follows:

() ={(x, x) : (y, z)(y, z), () ={(x, x) : (y)(y, y) }.

Note that () is equal to the identical relation if contains a fixed point, and () is equal to the empty relation otherwise. For these reasons, the operation can be considered as the descriptor of fixed points.

In the investigation of algebras of relations, one of the most important problem is the study their properties that can be expressed by identities. It leads us to consideration of varieties generated by classes of algebras of relations.

For any set of operations on relations, denote by R{} (R{, }) the class of algebras (partial ordered algebras) isomorphic to ones whose elements are binary relations and whose operations are members of. Let Var{} (Var{, }) be the variety generated by R{} (R{, }).

• Theorem 1. An algebra (A, ·,, ) of the type (2, 1, 1) belongs to the variety Var{,, } if and only if it satisfies the identities:

Pages:     | 1 |   ...   | 26 | 27 || 29 |

© 2011 www.dissers.ru - «Бесплатная электронная библиотека»

Материалы этого сайта размещены для ознакомления, все права принадлежат их авторам.
Если Вы не согласны с тем, что Ваш материал размещён на этом сайте, пожалуйста, напишите нам, мы в течении 1-2 рабочих дней удалим его.