检索结果-内蒙古大学图书馆

37th International workshop on Description Logics, DL 2024

作者： Snilsberg, Erik Karlsen, Leif Harald Kostylev, Egor V. Skjæveland, Martin G. Department of Informatics University of Oslo Norway

OTTR is a template language for the Semantic Web data and knowledge representation languages RDF and OWL. OTTR sees use as a key technology in the Semantic Web systems and already gained popularity both in academia and industry. OTTR is also in active development, which is, however, limited by the fact that little is known about its theoretical aspects. In this extended abstract we begin to close this gap by laying the foundations of OTTR. To this end, we first introduce a mathematical formalisation of the language in terms of its syntax and semantics. Then, we report bounds for the size of OTTR expansion—that is, of the data encoded by templates. Finally, we overview our study of the data and combined complexity of an important decision problem associated with the language and its fragments. © 2024 Copyright for this paper by its authors.

关键词： Latent semantic analysis

来源：评论

学校读者我要写书评

暂无评论

foundations of total functional data-flow programming 5

Foundations of total functional data-flow programming

引用

5th workshop on mathematically Structured Functional programming, MSFP 2014

作者： Trancón Y Widemann, Baltasar Lepper, Markus Ilmenau University of Technology de Germany GmbH de Germany

The field of declarative stream programming (discrete time, clocked synchronous, modular, datacentric) is divided between the data-flow graph paradigm favored by domain experts, and the functional reactive paradigm favored by academics. In this paper, we describe the foundations of a framework for unifying functional and data-flow styles that differs from FRP proper in significant ways: It is based on set theory to match the expectations of domain experts, and the two paradigms are reduced symmetrically to a low-level middle ground, with strongly compositional semantics. The design of the framework is derived from mathematical first principles, in particular coalgebraic coinduction and a standard relational model of stateful computation. The abstract syntax and semantics introduced here constitute the full core of a novel stream programming language.

关键词： Data flow graphs

来源：评论

学校读者我要写书评

暂无评论

Geometrical semantics for linear logic (multiplicative fragment)

引用

THEORETICAL COMPUTER SCIENCE 2006年第1-3期357卷 215-229页

作者： Slavnov, Sergey Cornell Univ Ithaca NY 14853 USA

Linear logic was described by Girard as a logic of dynamic interactions. On the other hand, Girard suggested an analogy between LL and quantum theory. Following these two intuitions we give an interpretation of linear logic in the language, which is common for both dynamical systems and quantization. Thus, we propose a denotational semantics for multiplicative linear logic using the language of symplectic geometry. We construct a category of coherent phase spaces and show that this category provides a model for MLL. A coherent phase space is a pair: a symplectic manifold and a distinguished field of contact cones on this manifold. The category of coherent phase spaces is a refinement of the symplectic "category" introduced by Weinstein. A morphism between two coherent phase spaces is a Lagrangian submanifold of their product, which is tangent to some distinguished field of contact cones. Thus, we interpret formulas of MLL as fields of contact cones on symplectic manifolds, and proofs as integral submanifolds of corresponding fields. In geometric and asymptotic quantization symplectic manifolds are phase spaces of classical systems, and Lagrangian submanifolds represent asymptotically states of quantized systems. Typically, a Lagrangian submanifold is the best possible localization of a quantum system in the classical phase space, as follows from the Heisenberg uncertainty principle. Lagrangian submanifolds are called sometimes "quantum points". From this point of view we interpret linear logic proofs as (geometric approximations to) quantum states and formulas as specifications for these states. In particular, the interpretation of linear negation suggests that the dual formulas A and A(perpendicular to) stand in the same relationship as the position and momentum observables. These two observables cannot simultaneously have definite values, much like the case of two dual formulas, which cannot simultaneously have proofs. (C) 2006 Published by Elsevier B.V.

关键词： linear logic denotational semantics

来源：评论

学校读者我要写书评

暂无评论

From truth to computability I

引用

THEORETICAL COMPUTER SCIENCE 2006年第1-3期357卷 100-135页

作者： Japaridze, Giorgi Villanova Univ Dept Comp Sci Villanova PA 19085 USA

The recently initiated approach called computability logic is a formal theory of interactive computation. It understands computational problems as games played by a machine against its environment, and uses logical formalism to describe valid principles of computability, with formulas representing computational problems and logical operators standing for operations on computational problems. The concept of computability that lies under this approach is a generalization of Church-Turing computability from simple, two-step (question/answer, input/output) problems to problems of arbitrary degrees of interactivity. Restricting this concept to predicates, which are understood as computational problems of zero degree of interactivity, yields exactly classical truth. This makes computability logic a generalization and refinement of classical logic. The foundational paper "Introduction to computability logic" [G. Japaridze, Ann. Pure Appl. Logic 123 (2003) 1-99] was focused on semantics rather than syntax, and certain axiomatizability assertions in it were only stated as conjectures. The present contribution contains a verification of one of such conjectures: a soundness and completeness proof for the deductive system CL3 which axiomatizes the most basic first-order fragment of computability logic called the finite-depth, elementary-base fragment. CL3 is a conservative extension of classical predicate calculus in the language which, along with all of the (appropriately generalized) logical operators of classical logic, contains propositional connectives and quantifiers representing the so called choice operations. The atoms of this language are interpreted as elementary problems, i.e. predicates in the standard sense. Among the potential application areas for CL3 are the theory of interactive computation, constructive applied theories, knowledgebase systems, systems for resource-bound planning and action. This paper is self-contained as it reintroduces all relevant definiti

关键词： computability logic interactive computation game semantics linear logic constructive logics knowledge bases

来源：评论

学校读者我要写书评

暂无评论

Correspondence Assertions for Process Synchronization in Concurrent Communications

引用

Electronic Notes in Theoretical Computer Science 2004年 97卷 175-195页

作者： Eduardo Bonelli Adriana Compagnoni Elsa Gunter Stevens Institute of Technology and LIFIA Faculty of Informatics University of La Plata La Plata Argentina Stevens Institute of Technology USA New Jersey Institute of Technology USA

High-level specification of patterns of communications such as protocols can be modeled elegantly by means of session types [Honda, K., V. Vasconcelos and M. Kubo, Language primitives and type discipline for structured communication-based programming, in: Proc. of ESOP'98, LNCS (1998), pp. 122–138]. However, a number of examples suggest that session types fall short when finer precision on protocol specification is required. In order to increase the expressiveness of session types we appeal to the theory of correspondence assertions [Clarke, E. and W. Marrero, Using formal methods for analyzing security, Information Survivability workshop (1998), Gordon, A. and A. Jeffrey, Typing correspondence assertions for communication protocols, in: Seventeenth Conference on the mathematical foundations of programming semantics (MFPS 2001), number 45 in ENTCS (2001)]. The resulting type discipline augments the types of long term channels with effects and thus yields types which may depend on messages read or written earlier within the same session. We prove that evaluation preserves typability and that well-typed processes are safe. Also, we illustrate how the resulting theory allows us to address the shortcomings present in the pure theory of session types. Keywords: Concurrent programming, pi-calculus, type systems, session types, correspondence assertions.

关键词： Concurrent programming pi-calculus type systems session types correspondence assertions

来源：评论

学校读者我要写书评

暂无评论

8th International workshop on Logic-Based Program Synthesis and Transformation, LOPSTR 1998

引用

8th International workshop on Logic-Based Program Synthesis and Transformation, LOPSTR 1998

ISBN: (纸本)3540657657

The proceedings contain 24 papers. The special focus in this conference is on Logic-Based Program Synthesis and Transformation. The topics include: Not just another logic specification language;a declarative semantics for mercury;pragmatics in the synthesis of logic programs;using decision procedures to accelerate domain-specific deductive synthesis systems;synthesis of programs in abstract data types;OOD frameworks in component-based software development in computational logic;the use of renaming in composing general programs;inductive synthesis of logic programs by composition of combinatory program schemes;specialising logic programs with respect to call/post specifications;generalization in hierarchies of online program specialization systems;improving homeomorphic embedding for online termination;successes in logic programs;inferring and compiling termination for constraint logic programs;strictness analysis as finite-domain constraint solving;invariant discovery via failed proof attempts;preventing instantiation errors and loops for logic programs with multiple modes using block declarations;algorithms for synthesizing reactive systems;schema-guided synthesis of CLP programs;proof planning with program schemas;logical synthesis of imperative O.-O. programs;mathematical foundations for program transformations;an exhaustive-search method using layered streams obtained through a meta-interpreter for chain programs and bottom-up specialisation of logic programs.

关键词：

来源：评论

学校读者我要写书评

暂无评论

Decidability of higher-order subtyping with intersection types 8th

Decidability of higher-order subtyping with intersection typ...

引用

8th workshop on Computer Science Logic, CSL 1994

作者： Compagnoni, Adriana B. Laboratory for Foundations of Computer Science Department of Computer Science University of Edinburgh United Kingdom

ISBN: (纸本)9783540600176

The combination of higher-order subtyping with intersection types yields a typed model of object-oriented programming with multiple inheritance [11]. The target calculus, F ⋀ω, a natural generalization of Girard's system F ω with intersection types and bounded polymorphism, is of independent interest, and is our subject of study. Our main contribution is the proof that subtyping in F ⋀ω is decidable. This yields as a corollary the decidability of subtyping in F ≤ω, its intersection free fragment, because the F ⋀ω subtyping system is a conservative extension of that of F ≤ω. The calculus presented in [8] has no reductions on types. In the F ⋀ω subtyping system the presence of β∧-conversion — an extension of β-conversion with distributivity laws — drastically increases the complexity of proving the decidability of the subtyping relation. Our proof consists of, firstly, defining an algorithmic presentation of the subtyping system of F ⋀ω, secondly, proving that this new presentation is sound and complete with respect to the original one, and finally, proving that the algorithm always terminates. Moreover, we establish basic structural properties of the language of types of F⋀ω such as strong normalization and Church-Rosser. Among the novel aspects of the present solution is the use of term rewriting techniques to present intersection types, which clearly splits the computational semantics (reduction rules) from the syntax (inference rules) of the system. Another original feature is the use of a choice operator to model the behavior of variables during subtype checking. © Springer-Verlag Berlin FIeidelberg 1995.

关键词： Computability and decidability

来源：评论

学校读者我要写书评

暂无评论

6th workshop on the mathematical foundations of programming semantics

6th Workshop on the Mathematical Foundations of Programming ...

引用

6th workshop on the mathematical foundations of programming semantics

This issue contains 9 conference papers. They cover: linear logic;domain theory;proof rules for fairness;Haginos categorical programming language;modal logic and algebraic specification;logic for category theory;logic... 详细信息

关键词： programming theory

来源：评论

学校读者我要写书评

暂无评论

workshop on the mathematical foundations of programming semantics (8th) Held at the University of Oxford on April 6-10, 1992.

Workshop on the Mathematical Foundations of Programming Sema...

引用

作者： Mislove, Michael W.

来源：评论

学校读者我要写书评

暂无评论

fourth workshop on mathematical foundations of programming semantics

Fourth Workshop on Mathematical Foundations of Programming S...

引用

fourth workshop on mathematical foundations of programming semantics

This issue contains 9 conference papers. The topics covered are: algebras, polynomials, and programs;functional polymorphism;fixed points in Cartesian closed categories;guarded theories;categorical fixed point semantics;functional completeness of mixed lambda-calculus and combinatory logic;recursive programs and denotational semantics in absolute logics of programs;Scott's thesis for domains of information and well-quasi-orderings;generalization of the concept of sketch. All papers are separately indexed and abstracted.

关键词： Computer programming

来源：评论

学校读者我要写书评

暂无评论

建议与咨询留下您的常用邮箱和电话号码，以便我们向您反馈解决方案和替代方法

时间限定

文献类型

馆藏选择

核心期刊

语言

文献类型

帮助

文字说明：

检索规则说明：

检索范例：

分类表

所选分类

限定检索结果

文献类型

馆藏范围

日期分布

学科分类号

主题

机构

作者

语言

请选择保存的检索档案：

请选择收藏分类：

通借通还

建议与咨询 留下您的常用邮箱和电话号码，以便我们向您反馈解决方案和替代方法

时间限定

文献类型

馆藏选择

核心期刊

语言

文献类型

帮助

文字说明：

检索规则说明：

检索范例：

分类表

所选分类

限定检索结果

文献类型

馆藏范围

日期分布

学科分类号

主题

机构

作者

语言

请选择保存的检索档案： 新增检索档案 确定 取消

请选择收藏分类： 新增自定义分类 确定 取消

通借通还

建议与咨询留下您的常用邮箱和电话号码，以便我们向您反馈解决方案和替代方法

请选择保存的检索档案：

请选择收藏分类：