Reasoning in Basic Description Logics and Description Logics with Modal Operators
Milenko Mosurović, Tatjana Stojanović, Ana Kaplarević-Mališić (2009)
Zbornik Radova
Similarity:
Milenko Mosurović, Tatjana Stojanović, Ana Kaplarević-Mališić (2009)
Zbornik Radova
Similarity:
Shira Elqayam (2005)
Philosophia Scientiae
Similarity:
Radosław Klimek (2014)
International Journal of Applied Mathematics and Computer Science
Similarity:
Giovanni Criscuolo (1996)
Mathware and Soft Computing
Similarity:
Radosław Klimek (2014)
International Journal of Applied Mathematics and Computer Science
Similarity:
The work concerns formal verification of workflow-oriented software models using the deductive approach. The formal correctness of a model's behaviour is considered. Manually building logical specifications, which are regarded as a set of temporal logic formulas, seems to be a significant obstacle for an inexperienced user when applying the deductive approach. A system, along with its architecture, for deduction-based verification of workflow-oriented models is proposed. The process...
Markovic, Zoran (1981)
Publications de l'Institut Mathématique. Nouvelle Série
Similarity:
Mariusz Giero (2016)
Formalized Mathematics
Similarity:
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...
Johan van Benthem (2007)
Publications de l'Institut Mathématique
Similarity:
Mariusz Giero (2015)
Formalized Mathematics
Similarity:
In the article [10] a formal system for Propositional Linear Temporal Logic (in short LTLB) with normal semantics is introduced. The language of this logic consists of “until” operator in a very strict version. The very strict “until” operator enables to express all other temporal operators. In this article we construct a formal system for LTLB with the initial semantics [12]. Initial semantics means that we define the validity of the formula in a model as satisfaction in the initial...
Barbara Dunin-Kęplicz, Linh Anh Nguyen, Andrzej Sza l as (2010)
Computer Science and Information Systems
Similarity:
Radoslaw Katarzyniak (2006)
International Journal of Applied Mathematics and Computer Science
Similarity:
A language grounding problem is considered for nonuniform sets of modal conjunctions consisting of conjunctions extended with more than one modal operator of knowledge, belief or possibility. The grounding is considered in the context of semiotic triangles built from language symbols, communicative cognitive agents and external objects. The communicative cognitive agents are assumed to be able to observe external worlds and store the results of observations in internal knowledge bases....
Zoran Ognjanović (2001)
Publications de l'Institut Mathématique
Similarity: