首页/论文/1603.09488

arXiv 1603.094882016-03-31cs.LOcs.AI

用MathSem程序构造集合论签名

Building the Signature of Set Theory Using the MathSem Program

UMCA Technologies（UMCA技术公司）

Andrey Luxemburg

阅读 PDF ↗

arXiv 页面 ↗HTML 原文 ↗

摘要英文摘要相关论文

摘要：

知识表示是信息技术中的一个热门研究领域，数学知识是形式化程度最高的知识，因此它的表示是一个重要而有趣的问题。数学知识是由各种数学理论组成的。在本文中，我们考虑一个演绎系统，推导数学概念，公理和定理。所有这些概念、公理和定理都可以看作是初等集合论的一部分。这个理论将被表示为语义网。

英文摘要：

Knowledge representation is a popular research field in IT. As mathematical knowledge is most formalized, its representation is important and interesting. Mathematical knowledge consists of various mathematical theories. In this paper we consider a deductive system that derives mathematical notions, axioms and theorems. All these notions, axioms and theorems can be considered as the part of elementary set theory. This theory will be represented as a semantic net.

机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。

阅读原文

阅读 PDF ↗

arXiv 页面 ↗HTML 原文 ↗

本文内容

摘要英文摘要相关论文

机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。

继续探索

相关论文

论论证框架、规范逻辑程序和抽象辩证框架的相对表达性

On the Relative Expressiveness of Argumentation Frameworks, Normal Logic Programs and Abstract Dialectical Frameworks

Computer Science Institute Leipzig University（莱比锡大学计算机科学研究所）

分析了抽象论证框架、规范逻辑程序和抽象辩证框架的二值语义的表达性。通过表达性，我们指的是在给定的命题签名上仅使用来自该签名的原子来编码所需的二值解释集合的能力。虽然所有这些语言的二值模型存在问题的计算复杂性是（几乎）相同的，我们表明，语言形成一个整洁的层次结构，就其表现力。

2014-05-05cs.AIcs.LO

事务处理逻辑程序的有效表列机制

Efficient Tabling Mechanisms for Transaction Logic Programs

Stony Brook University（石溪大学）；University of Toronto（多伦多大学）

在本文中，我们提出了有效的评估算法的霍恩事务逻辑（一个推广的定期霍恩逻辑程序与状态更新）。我们提出了两个互补的方法来优化事务逻辑的实现。第一种方法是基于制表和我们修改的证明理论表的状态调用和应答（实际上，相当于动态规划）。呼叫-应答表根据呼叫和进行呼叫的状态的签名进行索引。应答列包含应答统一和执行调用后状态的签名。使用基于尝试和计数的技术有效地对状态进行签名。第二种方法是基于增量评估，它适用于数据预言机包含派生关系。删除和插入（在事务oracle中执行）会更改数据库的状态。使用惯性的启发式（只有一部分状态响应于基本更新而变化），大多数时候只计算状态的变化比从头开始重新计算整个状态更便宜。这两种方法是互补的，因为第一种方法优化了在相同状态下重复调用时的评估，而第二种方法优化了在列表机制未找到调用-状态对时的新状态的评估（即第一种方法）。事务逻辑的证明理论应用了表格法和增量求值法，其模型理论是合理的、完整的。

2007-09-11cs.AIcs.LO

通用模块化逻辑程序

Generalizing Modular Logic Programs

CENTRIA - Centre for Artificial Intelligence（CENTRIA人工智能中心）；Universidade Nova de Lisboa（里斯本新大学）

尽管模块化在传统的逻辑编程中已经得到了广泛的研究，但关于如何将模块化纳入应答集编程（Answer Set Programming）的方法很少，应答集编程是一种基于规则的声明式编程范式。一个主要的方法是Oikarinnen和Janhunen的Gaifman-Shapiro风格的程序模块架构，它提供了程序模块的组成。他们的模定理适当地加强了Lifschitz和Turner的分裂集定理的正常逻辑程序。然而，这种方法受到模块条件的限制，这些条件是为了确保其模块系统与稳定模型语义的兼容性而施加的，即强制组成模块的输出签名不相交，并且不允许不同模块之间的正循环依赖。这些条件在实践中被证明是过于限制性的，在本文中，我们讨论的替代方法，解除这两个限制独立，有效地解决了第一个，扩大了这个框架的适用性和范围的模定理。

2014-04-29cs.AIcs.LO

保持强等价的选言逻辑程序的遗忘处理

An Approach to Forgetting in Disjunctive Logic Programs that Preserves Strong Equivalence

Simon Fraser University（西蒙弗雷泽大学）；Griffith University（格里菲斯大学）

在本文中，我们研究了遗忘的析取逻辑程序，其中忘记一个原子从一个程序相当于减少该程序的签名。我们的目标是提供一种语法独立的方法，如果两个程序是强等价的，那么每个程序中忘记一个原子的结果也应该是强等价的。我们对遗忘的中心定义是不切实际的，但满足了这个目标：遗忘一个原子的特征是程序的SE结果集，这些SE结果没有提到要被遗忘的原子。然后，我们提供了一个等效的、实用的定义，其中，遗忘原子$p$是由程序中不提及$p$的那些规则以及通过从提及$p$的规则中的单个推理步骤获得的规则给出的。遗忘被证明有适当的属性，以及，有限的表征结果在一个温和的（在最坏的二次）爆破。最后，我们也得到了一个原型实现这种方法的遗忘。

2014-04-29cs.AIcs.LO

表达性描述逻辑的基于签名的溯因--技术报告

Signature-Based Abduction for Expressive Description Logics -- Technical Report

Technische Universität Dresden（德累斯顿工业大学）；The University of Manchester（曼彻斯特大学）；Max Planck Institut für Informatik（马克斯·普朗克计算机科学研究所）

基于特征的溯因推理旨在对一组特定的名字（特征）建立假设，这些假设解释了与某些背景知识相关的观察。这种类型的外展对于诊断等任务很有用，其中用于观察症状的词汇与预期解释这些症状的词汇不同。我们提出了第一个完整的方法解决基于签名的溯因表达的描述逻辑ALC中表示的意见，其中可以包括TBox和ABox公理，从而解决知识库溯因问题。该方法是保证计算一个有限的和完整的假设集，并在一组现实的知识库进行评估。

2020-07-08cs.AIcs.LO

答案集编程入门

A primer on Answer Set Programming

一本关于答案集编程的语法和语义的介绍，作为讲义给正在学习人工智能或逻辑编程课程的研究生。

2005-08-23cs.AIcs.LO

更多相关论文收起更多论文

在LANA中注释用户集程序？

Annotating Answer-Set Programs in LANA?

University of Bath（巴斯大学）；Sabanci University（萨班哲大学）；Technische Universität Wien（维也纳工业大学）

虽然过去的研究在回答集编程（ASP）主要集中在理论，ASP求解器技术，和应用程序，目前的工作本身的背景下，一个相当最近的研究趋势：开发支持ASP。特别是，我们建议增加答案集程序与额外的元信息制定一个专用的注释语言，称为LANA。这种语言允许将规则分组为连贯的块，并指定语言签名、类型、前置和后置条件，以及这些块的单元测试。虽然这些注释对ASP求解器是不可见的，因为它们采取程序注释的形式，但它们可以被工具解释为文档，测试和验证目的，以及通过实现语法检查或代码完成功能来消除常见编程错误的来源。为了证明它的多功能性，我们介绍了两个这样的工具，即（一）ASPDOC，用于生成一个HTML文档的基础上的注释信息的程序，和（二）ASPUNIT，用于运行和监控程序块上的单元测试。在基于Eclipse的ASP集成开发环境SeaLion系统中，也对LANA进行了开发。逻辑程序设计理论与实践Theory and Practice of Logic Programming

2012-10-08cs.AIcs.SE

onlineSPARC：一个应答集编程环境

onlineSPARC: a Programming Environment for Answer Set Programming

Tufts University（塔夫茨大学）；Texas Tech University（得克萨斯理工大学）

逻辑编程的最新进展（例如，答案集编程范例的发展）使得将其教授给普通大学生甚至初中/高中学生成为可能。鉴于这些学生接触计算机科学的机会有限，下载、安装和使用编写逻辑程序的工具的复杂性可能是逻辑编程接触更广泛受众的主要障碍。我们开发了一个在线的答案集编程环境，一个自包含的文件系统和一个简单的界面。它允许用户键入/编辑逻辑程序，并在程序上执行几项任务，包括对程序进行查询，获取程序的答案集，以及基于程序的答案集生成绘图/动画。

2018-09-21cs.AI

逻辑解释在程序开发中的作用

The role of logical interpretations in program development

代数规格说明的逐步精化是程序开发的一种著名的形式化方法。然而，传统的概念，细化的基础上签名态射往往过于僵化，以捕捉一些相关的软件设计，重用和适应的背景下的转换。本文提出了一种新的加细方法，在这种方法中，签名态射被逻辑解释所取代，作为证明加细的一种手段。该方法首先在方程逻辑的背景下，后来推广到任意维度的演绎系统。这允许，例如，细化成方程式规格和后者到模态的。

2014-01-29cs.LO

变量绑定中语法和操作语义的签名和模型

Signatures and models for syntax and operational semantics in the presence of variable binding

本文研究了程序设计语言的语法和操作语义的规范和构造。我们使用签名的一般概念来指定给定类别的对象作为合适类别的模型中的初始对象。这种表征，在初始语义学的精神中，给出了递归原则的理由。带有变量绑定的语言，例如纯λ演算，是通过经典代数签名指定的集合范畴上的单子。第一次扩展语法与方程，我们认为是这些代数签名的继承人。例如，它们允许指定二元交换操作。但有些方程，如结合论，似乎仍然遥不可及。因此，我们介绍的概念2签名，包括两个部分：规范的操作，通过一个通常的签名，如前所述，和一组方程。我们确定的代数2-签名类的存在相关联的语法是有保证的。最后，我们给出了一种程序设计语言（如λ演算）的操作语义的规范化描述。为此，我们引入了约简单子及其签名的概念，并将其推广为运算单子的概念。

2019-12-18cs.LO

非确定性程序的代数：恶魔算子、序和公理

The algebra of non-deterministic programs: demonic operators, orders and axioms

恶魔组合、恶魔精炼和恶魔联盟是通常的“天使”组合、天使精炼（包含）和天使（通常）联盟的替代品。我们首先激励天使和恶魔通过非确定性程序的行为分析，与天使与部分正确性和恶魔与总正确性，这两种情况下出现的非确定性程序的一个更丰富的代数模型，将这两个方面。Zareckii证明了二元关系代数在天使合成和包含下的同构类被公理化为序半群类。这个证明可以用来建立同样的公理化适用于恶魔合成和细化下的二元关系，并且证明的进一步修改可以用来包含一个零元素，代表天使情况下的空关系和恶魔情况下的全关系。对于签名的天使组成和工会，它是已知的，没有有限的公理化存在，我们显示了类似的结果，恶魔组成和恶魔工会显示，相同的公理化持有两者。我们表明，同构类代数的二元关系的“混合”签名的恶魔组成和天使般的包含没有有限axiomatisation。作为对比，我们证明了具有星座积和包含（也是一个“混合”签名）的部分运算的二元关系的部分代数的同构类是可公理化的。

2021-01-13cs.CLcs.LO

通过静态可达性分析挖掘恶意软件规范

Mining Malware Specifications through Static Reachability Analysis

LIAFA, CNRS（法国国家科学研究中心LIAFA实验室）；Univ. Paris Diderot（巴黎狄德罗大学）

恶意软件（malware）的数量正在失控地增长。基于句法签名的检测无法应对这种增长，并且恶意软件签名数据库的手动构建需要被基于计算机学习的方法所取代。目前，捕获恶意行为语义的单个现代签名可以用来替换任意大量的老式语法签名。然而，教计算机学习此类行为是一项挑战。现有的恶意行为提取方法主要依赖于动态分析，但这种方法不能保证对所有恶意行为的覆盖。为了避开这个限制，我们展示了如何使用静态可达性分析来学习恶意软件签名。其思想是使用下推系统（可用于对二进制代码执行期间发生的堆栈操作进行建模）对二进制程序进行建模，使用可达性分析以树的形式提取行为，并使用从恶意软件文件的训练集中提取的树中常见的子树作为签名。为了检测恶意软件，我们建议使用树自动机来压缩存储恶意行为树，并检查从分析文件中提取的任何子树是否是恶意的。实验数据表明，我们的方法可以用来学习从恶意软件文件的训练集的签名，并使用它们来检测一个测试集的恶意软件是5倍的训练集的大小。

2013-12-17cs.AIcs.CRcs.LO

可呈现的签名与初始语义

Presentable signatures and initial semantics

本文提出可呈现签名框架，用于指定数据类型和编程语言语法，通过初始语义生成语法，涵盖变量绑定并支持组合构造，且经计算机验证。

2021-05-25cs.LOcs.PL

基于应答集程序的命令式程序合成

Imperative Program Synthesis from Answer Set Programs

我们的研究关注的是从答案集编程规范生成命令式程序。ASP是高度声明性的，是编写规范的理想选择。此外，利用否定即失败，很容易简洁地表示组合搜索问题。我们目前正致力于从ASP程序中合成命令式程序，将否定转换为有用的计算。这开辟了一种新的方式来合成程序的可执行规范。

2019-09-19cs.LOcs.SC

$\{log\}$：将公式设置为程序

$\{log\}$: Set Formulas as Programs

$\{log\}$是一种程序设计语言，介于约束逻辑编程、集合编程和声明式编程之间。但是$\{log\}$也是有限集合和有限二元关系理论的可满足性求解器。有了$\{log\}$，程序员可以使用集合论和二元关系的所有功能编写抽象程序。这些程序不是很有效，但它们非常接近规范。其正确性更加明显。此外，$\{log\}$程序也是设定的公式。因此，程序员可以再次使用$\{log\}$来自动证明他们的程序验证非平凡属性。在本文中，我们通过几个例子来展示这种开发方法。

2021-04-16cs.LOcs.PLcs.SE