China
Africa
Explore chapters and articles related to this topic
Communication systems and network technologies
Published in Kennis Chan, Future Communication Technology and Engineering, 2015
Many approaches for knowledge representation and reasoning have been proposed using the Logic Programming (LP) archetype, namely in the area of Model Theory (Kakas et al., 1998, Pereira & Anh, 2009), and Proof Theory (Neves, 1984, Neves et al., 2007). We follow the proof theoretical approach and an extension to the LP language, to knowledge representations and reasoning. An Extended Logic Program is a finite set of clauses in the form: p←p1,⋯,pn,notq1,⋯,notqm?p1,⋯,pn,notq1,⋯,notqm(n,m≥0)
Logical dual concepts based on mathematical morphology in stratified institutions: applications to spatial reasoning
Published in Journal of Applied Non-Classical Logics, 2019
There exists a profusion of logics but all of them satisfy the same structure defined by a syntax, a semantics and a calculus. Syntax gives both the language (signatures) and the formal rules that define well-formed formulas and theories. Semantics, so-called model theory, gives the mathematical meaning of all these syntactic notions, among others the rules that associate truth values to formulas. Finally, calculus, so-called proof theory, gives the inference rules that govern the reasoning and thus translate semantics into syntax as correctly as possible. To cope with the explosion of logics, a categorical abstract model-theory, the theory of institutions (Diaconescu, 2008; Goguen & Burstall, 1992), has been proposed, that generalises Barwise's ‘Translation Axiom’ (Barwise, 1974). Institutions then define both syntax and semantics of logics at an abstract level, independently of commitment to any particular logic. Later, institutions have been extended to propose a syntactic approach to truth (Diaconescu, 2006, 2008; Fiadeiro & Sernadas, 1988; Meseguer, 1989). For the sake of generalisation, in institutions signatures are simply defined as objects of a category and formulas built over signatures are simply required to form a set. All other contingencies such as inductive definition of formulas are not considered. However, in concrete logics (anyway all the particular logics considered in this paper as examples), the reasoning (both syntactic and semantic) is defined by induction on the structure of formulas. Indeed, usually, formulas are built from ‘atomic’ formulas by applying iteratively operators such as connectives, quantifiers or modalities. What we can then observe is that most of these logical operators come through dual pairs (conjunction and disjunction ∧ and ∨, quantifiers ∀ and ∃, modalities and ⋄).