Wyniki wyszukiwania - Biblioteka Nauki

Nowa wersja platformy, zawierająca wyłącznie zasoby pełnotekstowe, jest już dostępna.
Przejdź na https://bibliotekanauki.pl

Ograniczanie wyników

5 Formalized Mathematics

Znaleziono wyników: 5

Liczba wyników na stronie

Wyniki wyszukiwania

Sortuj według:

Ogranicz wyniki do:

The Axiomatization of Propositional Logic

100%

Giero M.

nr 4

281-290

This article introduces propositional logic as a formal system ([14], [10], [11]). The formulae of the language are as follows φ ::= ⊥ | p | φ → φ. Other connectives are introduced as abbrevations. The notions of model and satisfaction in model are defined. The axioms are all the formulae of the following schemes α ⇒ (β ⇒ α), (α ⇒ (β ⇒ γ)) ⇒ ((α ⇒ β) ⇒ (α ⇒ γ)), (¬β ⇒ ¬α) ⇒ ((¬β ⇒ α) ⇒ β). Modus ponens is the only derivation rule. The soundness theorem and the strong completeness theorem are proved. The proof of the completeness theorem is carried out by a counter-model existence method. In order to prove the completeness theorem, Lindenbaum’s Lemma is proved. Some most widely used tautologies are presented.

Weak Completeness Theorem for Propositional Linear Time Temporal Logic

100%

Giero M.

nr 3

227-234

We prove weak (finite set of premises) completeness theorem for extended propositional linear time temporal logic with irreflexive version of until-operator. We base it on the proof of completeness for basic propositional linear time temporal logic given in [20] which roughly follows the idea of the Henkin-Hasenjaeger method for classical logic. We show that a temporal model exists for every formula which negation is not derivable (Satisfiability Theorem). The contrapositive of that theorem leads to derivability of every valid formula. We build a tree of consistent and complete PNPs which is used to construct the model.

The Properties of Sets of Temporal Logic Subformulas

100%

Giero M.

nr 3

221-226

This is a second preliminary article to prove the completeness theorem of an extension of basic propositional temporal logic. We base it on the proof of completeness for basic propositional temporal logic given in [17]. We introduce two modified definitions of a subformula. In the former one we treat until-formula as indivisible. In the latter one, we extend the set of subformulas of until-formulas by a special disjunctive formula. This is needed to construct a temporal model. We also define an ordered positive-negative pair of finite sequences of formulas (PNP). PNPs represent states of a temporal model.

The Derivations of Temporal Logic Formulas

100%

Giero M.

nr 3

215-219

This is a preliminary article to prove the completeness theorem of an extension of basic propositional temporal logic. We base it on the proof of completeness for basic propositional temporal logic given in [12]. We introduce n-ary connectives and prove their properties. We derive temporal logic formulas.

The Formalization of Decision-Free Petri Net

51%

Shah P. K. , Kawamoto P. N. , Giero M.

nr 1

29-35

In this article we formalize the definition of Decision-Free Petri Net (DFPN) presented in [19]. Then we formalize the concept of directed path and directed circuit nets in Petri nets to prove properties of DFPN. We also present the definition of firing transitions and transition sequences with natural numbers marking that always check whether transition is enabled or not and after firing it only removes the available tokens (i.e., it does not remove from zero number of tokens). At the end of this article, we show that the total number of tokens in a circuit of decision-free Petri net always remains the same after firing any sequences of the transition.