Wyniki wyszukiwania - BazTech

1

Extending Logic Programming with Labelled Variables : Model and Semantics

Calegari R., Denti E., Dovier A., Omicini A.

Fundamenta Informaticae

|

2018

|

Vol. 161, nr 1/2

53--74

EN

In order to enable logic programming to deal with the diversity of pervasive systems, where many heterogeneous, domain-specific computational models could benefit from the power of symbolic computation, we explore the expressive power of labelled systems. To this end, we define a new notion of truth for logic programs extended with labelled variables interpreted in non-Herbrand domains-where, however, terms maintain their usual Herbrand interpretations. First, a model for labelled variables in logic programming is defined. Then, the fixpoint and the operational semantics are presented and their equivalence is formally proved. A meta-interpreter implementing the operational semantics is also introduced, followed by some case studies aimed at showing the effectiveness of our approach in selected scenarios.

2

Type Theories and Lexical Networks : using Serious Games as the basis for Multi-Sorted Typed Systems

Chatzikyriakidis S., Lafourcade M., Ramadier L., Zarrouk M.

Journal of Language Modelling

|

2017

|

Vol. 5, No. 2

229--272

EN

In this paper, we show how a rich lexico-semantic network which Has been built using serious games, JeuxDeMots, can help us in grounding our semantic ontologies in doing formal semantics using rich or modern type theories (type theories within the tradition of Martin Löf). We discuss the issue of base types, adjectival and verbal types, hyperonymy/hyponymy relations as well as more advanced issues like homophony and polysemy. We show how one can take advantage of this wealth of lexical semantics in a formal compositional semantics framework. We argue that this is a way to sidestep the problem of deciding what the type ontology should look like once a move to a many sorted type system has been made. Furthermore, we show how this kind of information can be extracted from a lexico-semantic Network like JeuxDeMots and inserted into a proof-assistant like Coq in order to perform reasoning tasks.

3

A Formal and Unified Description of XML Manipulation Languages

Hidders J., Paredaens J.

Fundamenta Informaticae

|

2016

|

Vol. 145, nr 4

429--470

EN

We discuss three well-known languages for querying and manipulatingXML documents: XQuery, XPath and XSLT. They are considered to be the standard languages for processing XML documents. However, specifying their complete semantics in a formal way seems almost impossible. Indeed, an attempt by the W3C XML Query Working Group to do so for XQuery was ultimately abandoned. We introduce three sublanguages, called MiXPath, MiXQuery and MiXSLT, and describe their syntax and formal semantics. The syntax and semantics of these languages are chosen such that they are consistent with the ones given in the relatedW3C recommendations. As such this provides a practical foundation for research and teaching of XML languages. For this purpose the sublanguages are chosen such that they contain the most crucial features, constructs and expressions of each of these three languages.

4

Towards a Formal Semantics for the Process Model of the Taverna Workbench. Part I

Sroka J., Hidders J.

Fundamenta Informaticae

|

2009

|

Vol. 92, nr 3

279-299

EN

Workflow development and enactment workbenches are becoming a standard tool for conducting in silico experiments. Their main advantages are easy to operate user interfaces, specialized and expressive graphical workflow specification languages and integration with a huge number of bioinformatic services. A popular example of such a workbench is Taverna, which has many additional useful features like service discovery, storing intermediate results and tracking data provenance. We discuss a detailed formal semantics for Scufl - the workflow definition language of the Taverna workbench. It has several interesting features that are notmet in other models including dynamic and transparent type coercion and implicit iteration, control edges, failure mechanisms, and incominglinks strategies. We study these features and investigate their usefulness separately as well as in combination, and discuss alternatives. The formal definition of such a detailed semantics not only allows to exactly understand what is being done in a given experiment, but is also the first step toward automatic correctness verification and allows the creation of auxiliary tools that would detect potential errors and suggest possible solutions to workflow creators, the same way as Integrated Development Environments aid modern programmers. A formal semantics is also essential for work on enactment optimization and in designing the means to effectively query workflow repositories. This paper is the first of two. It defines, explains and discusses fundamental notions for describing Scufl graphs and their semantics. Then, in the second part, we use these notions to define the semantics and show that our definition can be used to prove properties of Scufl graphs.

5

Towards a Formal Semantics for the Process Model of the Taverna Workbench. Part II

Sroka J., Hidders J.

Fundamenta Informaticae

|

2009

|

Vol. 92, nr 4

373-396

EN

Workflow development and enactment workbenches are becoming a standard tool for conducting in silico experiments. Their main advantages are easy to operate user interfaces, specialized and expressive graphical workflow specification languages and integration with a huge number of bioinformatic services. A popular example of such a workbench is Taverna, which has many additional useful features like service discovery, storing intermediate results and tracking data provenance. We discuss a detailed formal semantics for Scufl - the workflow definition language of the Taverna workbench. It has several interesting features that are notmet in other models including dynamic and transparent type coercion and implicit iteration, control edges, failure mechanisms, and incominglinks strategies. We study these features and investigate their usefulness separately as well as in combination, and discuss alternatives. The formal definition of such a detailed semantics not only allows to exactly understand what is being done in a given experiment, but is also the first step toward automatic correctness verification and allows the creation of auxiliary tools that would detect potential errors and suggest possible solutions to workflow creators, the same way as Integrated Development Environments aid modern programmers. A formal semantics is also essential for work on enactment optimization and in designing the means to effectively query workflow repositories. This paper is the second of two. In the first one [13] we have defined, explained and discussed fundamental notions for describing Scufl graphs and their semantics. Here, in the second part, we use these notions to define the semantics and show that our definition can be used to prove properties of Scufl graphs.

6

Autonomous Units to Model Interacting Sequential and Parallel Processes

Hölscher K., Kreowski H-J., Kuske S.

Fundamenta Informaticae

|

2009

|

Vol. 92, nr 3

233-257

EN

In this paper, we introduce the notion of a community of autonomous units as a rulebased and graph-transformational device to model processes that run interactively but independently of each other in a common environment. The main components of an autonomous unit are a set of rules, a control condition, and a goal. Every autonomous unit transforms graphs by applying its rules so that the control condition is satisfied. If the goal is reached the resulting transformation process is successful. A community contains a set of autonomous units, an initial environment specification, and an overall goal. In every transformation process of a community the autonomous units interact via their common environment. As an example, the game Ludo is modeled as a community of self-controlled players who interact on a common board. The emphasis of the presented approach is laid on the study of the formal semantics of a community as a whole and of each of its member units separately. In particular, a sequential as well as a parallel semantics is introduced, and communities with parallel semantics are compared with Petri nets, cellular automata, and multiagent systems.

7

A Formal Syntax of Natural Languages and the Deductive Grammar

Wang Y.

Fundamenta Informaticae

|

2009

|

Vol. 90, nr 4

353-368

EN

This paper presents a formal syntax framework of natural languages for computational linguistics. The abstract syntax of natural languages, particularly English, and their formal manipulations are described. On the basis of the abstract syntax, a universal language processing model and the deductive grammar of English are developed toward the formalization of Chomsky's universal grammar in linguistics. Comparative analyses of natural and programming languages, as well as the linguistic perception on software engineering, are discussed. A wide range of applications of the deductive grammar of English have been explored in language acquisition, comprehension, generation, and processing in cognitive informatics, computational intelligence, and cognitive computing.

8

Generalized Interpolation in First Order Logic

Borzyszkowski T.

Fundamenta Informaticae

|

2005

|

Vol. 66, nr 3

199--219

EN

We consider the Craig Interpolation Property for many sorted first-order logic. The Craig Interpolation Property explored in this paper is inspired by the institution independent generalization of this property presented in [21]. In [3] the author presents the interpolation result for the institution of many sorted first-order logic, with both morphisms in the pushout square being injective on sort names. The author also shows that the Craig Interpolation Property does not hold when both morphisms are certain morphisms which are noninjective on sort names. An open question in that paper was whether the interpolation property holds with only one morphism being injective on sort names. In this paper we give answer to this question. Following the overall structure of the classical proof presented in [7] for single sorted first-order logic, but with new technicalities concerning the many sorted case, we show that many sorted first-order logic has the interpolation property when just one (left or right) morphism is injective on sort names.

9

Discourse interpretation based on dynamic constraints

Piasecki M.

Archives of Control Sciences

|

2005

|

Vol. 15, no. 3

403-414

EN

Our main objective will be to construct a fully compositional representation of nominal anaphora in discourse. The proposed representation is not dependent on the remote ascription (i.e. done outside the formal representation) of syntactic indexes, which identify anaphoric links. A formal language of variable free logic is introduced. It is based on dynamic semantics paradigm and is a variant of many-sorted type logic. We will also present the scope free treatment of quantification in multiple quantifier sentences. The interpretation of multiple quantifiers is defined by means of a construction of the polyadic Generalised Quantifier (GQ). The polyadic GQ is a constraint that should be satisfied by the denotation of a ?clausal? predicate.

10

Assessing trust in the semantic Web

Juszczyszyn K., Sachse P.

Systems Science

|

2004

|

Vol. 30, no 1

99-114

EN

The concept of semantic Web - a new WWW architecture that enhances content with formal semantics and machine-understandable meta data - is briefly presented. Then trusted behaviour of agents in this, fundamentally dynamic, environment is discussed. The paper proposes a probabilistic approach for trust assessing and representation. The methods of comparing probability-based trust levels are also presented. Our approach postulates a simple representation of trust primitives (sets of ratings) which are then used by more sophisticated methods. The proposed solution is also flexible and allows each of the network agents to conduct its own trust policy.