Infinitary Classical Logic: Recursive Equations and Interactive Semantics
在本文中，我们提出了一个经典逻辑的无限扩展派生的交互语义。我们语言的公式可能是由命题变量和逻辑连接词标记的无限树。我们表明，在我们的设置每个递归公式方程有一个唯一的解决方案。至于导子，我们使用Tait演算的无穷变体来导出序列。我们在本文中介绍的派生的交互式语义被表示为测试<< T >>（派生候选者，Proponent）和环境<< not S >>（否定对象，Opponent）之间的辩论（交互树）。我们证明了一个推导的完备性定理，我们称之为交互完备性定理：<< T >>（测试）和<< not S >>（环境）之间的交互不会产生错误（即，Proponent wins）以防<< T >>来自< >的句法派生< S >。
2014-09-11 cs.LO
Interactive Logic Programming via Choice-Disjunctive Clauses
在逻辑编程中添加交互是一项重要任务。线性逻辑等表达逻辑为这种机制提供了理论基础。不幸的是，没有一个现有的线性逻辑语言可以建模与用户的交互。这是因为他们使用可证明性作为计算的唯一基础。我们建议使用游戏的语义，而不是可证明性作为计算的基础，让用户更积极的参与。我们说明我们的想法通过muprolog，一个扩展的Prolog与选择析取子句。
2015-07-12 cs.LO
Paraconsistency of Interactive Computation
计算逻辑的目标是使我们能够对计算进行建模和推理，我们认为计算逻辑必须能够对交互式计算进行建模。我们表明，一阶逻辑不能模拟交互式计算，由于交互的不完整性。我们表明，交互式计算必然是次协调的，能够模拟的事实和它的否定，由于世界（环境）的作用，在确定的过程中的计算。我们的结论是，次协调是一个必要的属性的逻辑，可以模拟交互式计算。
2002-07-21 cs.LO
GeoLogic -- Graphical interactive theorem prover for Euclidean geometry
计算机中的数理逻辑领域主要由自动定理证明器（ATP）和交互式定理证明器（ITP）控制。这两种方法都很难被人工智能从人类模仿的方法中获得：ATP通常使用对人类不友好的逻辑基础，而ITP则用于形式化现有的证明，而不是解决问题。我们的目标是创建一个简单的人类友好的数学问题解决逻辑系统。我们选择了欧几里得几何的案例研究，因为它可以很容易地可视化，具有简单的逻辑，但可能会提供许多不同难度的高中问题。为了使环境对用户友好，我们放弃了ITP所要求的严格逻辑，允许从图片中推断拓扑事实。我们提出了我们的系统为欧几里德几何，连同一个图形应用程序GeoLogic，类似GeoGebra，它允许用户交互式地研究和证明几何设置的属性。
2020-05-07 cs.LO
Interactive Unawareness Revisited
我们分析了海菲兹，迈耶和席佩尔（HMS）介绍的互动无意识模型。我们考虑两个公理化的模型，捕捉不同的概念的有效性。这些公理化使我们能够比较HMS方法的标准（S5）认知逻辑和其他两种方法的无意识：费金和Halpern和莫迪卡和Rustichini。我们发现，HMS方法和其他之间的差异主要是由于使用的有效性的概念和事实，即HMS是基于一个3值命题逻辑。
2005-09-19 cs.AI cs.LO
A sound spatio-temporal Hoare logic for the verification of structured interactive programs with registers and voices
具有寄存器和语音的交互式系统（简称“rv系统”）是一种用于交互式计算的模型，该模型相对于时空对偶变换获得了闭寄存器机（“语音”是“寄存器”的时间对偶对应物）。同样的，AGAPIA v0.1，一种用于rv系统的结构化程序设计语言，是经典while程序（针对特定类型的数据）的时空对偶闭包。典型的AGAPIA程序描述了位于不同地点的开放过程，并具有对环境做出适当反应的时间窗口。该语言自然地支持流程迁移、结构化交互和在异构机器上部署组件。本文介绍了一种用于验证AGAPIA v0.1程序的类Hoare时空逻辑。作为一个案例研究，一个流行的分布式终止检测协议的形式化验证证明。
2008-10-19 cs.LO cs.PL
Towards Interactive Logic Programming
线性逻辑编程使用可证明性作为计算的基础。在基于可证明性的操作语义中，如果$G_1$和$G_2$都可从$P$求解，则从程序$P$执行加性-合取目标$G_1 \& G_2$简单地以成功终止。这是一种不令人满意的情况，因为在这种语义中缺少\&的中心动作--用户选择$G_1$或$G_2$的动作。我们建议修改上面的操作语义以允许用户更积极地参与。我们说明了我们的想法，通过muProlog，Prolog的扩展添加剂的目标。
2015-07-01 cs.LO cs.PL
The Abella Interactive Theorem Prover (System Description)
Abella是一个交互式系统，用于推理对象语言的各个方面，这些方面已经通过基于语法结构的递归规则正式呈现。Abella使用两级逻辑方法来规范和推理。一个级别由规范逻辑定义，该规范逻辑支持结构语义规则的透明编码，并且还支持它们的执行。第二个层次，称为推理逻辑，嵌入规范逻辑，并允许开发有关规范的属性的证明。这两种逻辑的一个重要特征是，它们利用lambda树语法方法来处理对象语言中的绑定。除此之外，Abella还被用来证明λ演算的正规化性质、λ演算的截容许性、类型唯一性和主体归约性质。本文讨论了Abella的逻辑基础，概述了它支持的定理证明的风格，最后描述了它最近的一些应用。
2008-05-23 cs.LO cs.PL
Logic of Non-Monotonic Interactive Proofs (Formal Theory of Temporary Knowledge Transfer)
我们提出了一个单调逻辑的内部化非单调或即时交互证明（LiiP）和重建现有的单调逻辑的内部化单调或持久交互证明（LiP）作为一个最小的保守扩展LiiP。即时交互式证明在其预期的同行评审者社区中产生了脆弱的认识影响，这种影响在于通过与解释评审者的证明知识对他们的证明目标的知识的短暂归纳：如果我的同行评审者知道我的证明，那么她至少会（在那一瞬间）知道它的证明目标是正确的。它们的影响是脆弱的，它们对知识的归纳也是短暂的，因为它可能只在学习证明的瞬间才存在。这就解释了将真值可以变化的陈述的证明内在化的重要可能性，与不变陈述相反，这些陈述不能有持久的证明。因此，即时交互证明通过在多个交互代理的分布式系统中传输某些个人知识（可知的非单调证明）来实现某些命题知识（可知的短暂事实）的临时转移。
2013-01-31 cs.CR cs.DC cs.LO
Iltis: Learning Logic in the Web
Iltis项目提供了一个交互式的、基于网络的系统，用于教授形式方法的基础。其目的是允许简单地纳入新的教育任务;将这些任务纳入更复杂的练习;并允许简单地纳入和级联反馈机制。目前，许多典型的自动推理工作流程的命题逻辑，模态逻辑和一阶逻辑的某些部分的练习都包括在内。最近，Iltis已经达到了一个成熟的水平，大部分的入门逻辑课程可以补充互动练习。在过去几年中，设计了互动式教材样本，并在课程中使用，其中许多课程的学生超过300人。我们邀请所有读者试用Iltis：https://iltis.cs.tu-dortmund.de
2022-05-27 cs.LO
An interactive semantics of logic programming
我们适用于逻辑编程的一些最近出现的想法，从该领域的减少为基础的通信系统，目的是提供证据的隐藏的相互作用和协调机制，规则的运作机制，这样的编程范式。语义框架，我们选择了我们的结果是瓦片逻辑，它的优点是允许一个统一的治疗目标和意见，并应用抽象的分类工具来证明结果。作为主要的贡献，我们提到的有限表示的抽象统一，和并发和协调的抽象语义逻辑编程的最常见的语义相一致。此外，拼块语义的组合性由标准结果保证，因为它减少了对与逻辑程序相关联的拼块系统享有拼块分解属性的检查。还讨论了处理约束系统的方法的扩展。
2001-07-17 cs.LO cs.PL
A Formal Approach based on Fuzzy Logic for the Specification of Component-Based Interactive Systems
形式化方法被广泛认为是分布式交互系统的规范、仿真、开发和验证的一种强有力的工程方法。然而，大多数形式化方法依赖于二值逻辑，因此受限于该逻辑的公理：规范有效或无效，组件行为可实现或不可实现，安全属性保持或被违反，系统可用或不可用。特别是当问题域具有不确定性，不精确性和不确定性时，这些方法的应用成为一项具有挑战性的任务。为了克服形式化方法的严格工作方式所带来的局限性，本文的主要目的是通过使用模糊逻辑来放松形式化规范的布尔概念。本方法是基于焦点理论，一个基于模型的和严格的形式化方法，基于组件的交互式系统。这项工作的贡献是双重的：i）我们引入了规范技术的基础上，模糊逻辑，可用于顶部的焦点开发正式规范的定性方式; ii）我们部分扩展焦点理论的模糊，它允许规范的模糊组件和模糊的相互作用。虽然前者提供了一种方法来近似I/O行为下的不精确性，后者能够捕捉到一个更定量的规格属性，如可实现性。
2015-03-17 cs.LO cs.SE
Logic of Negation-Complete Interactive Proofs (Formal Theory of Epistemic Deciders)
我们产生了一个可判定的经典正常模态逻辑的内在否定完全，从而析取非单调交互式证明（LDiiP）从现有的逻辑对应的非单调或即时交互式证明（LiiP）。LDiiP内化了以主体为中心的证明论，这些理论是否定完备的（最大的）和一致的（因此严格弱于例如皮亚诺算术），并享有析取属性（如直觉主义逻辑）。换句话说，内化证明论是超过滤器，所有内化证明目标都是确定的，通过析取内化证明（因此也称为认识决定者）对代理人来说是可证明或不可证明的。尽管如此，LDiiP本身是经典的（单调的，非构造性的），负不完全的，并且不具有析取性质。我们的交互式证明的否定完全性的代价是它们的非单调性和非公共性（仅适用于单例代理社区）。作为一个正常的模态逻辑，LDiiP享有一个标准的Kripke语义，我们证明通过调用选择公理的LiiP的，然后构造一个具体的预言计算功能。LDiiP的以代理人为中心的内在化证明概念也可以被视为标准KD 45信念的否定完全析取显式精化，并产生S4可证明性的析取但否定不完全显式精化。
2013-05-29 cs.CR cs.DC cs.LO
Logic of Intuitionistic Interactive Proofs (Formal Theory of Perfect Knowledge Transfer)
我们产生了一个可判定的超直觉正常模态逻辑的内在直觉（从而析取和单调）交互式证明（LIIP）从现有的经典对应的经典单调非析取交互式证明（LiP）。直觉主义交互式证明在可能的对抗性通信媒介CM（被想象为一个杰出的代理人）中产生持久的认知影响，并且只有在这种情况下，它才包括通过CM的证明知识永久地归纳出他们的证明目标的完美知识和分离知识：如果CM知道我的证明，那么CM将持续地并且分离地知道我的证明目标是真的。因此，直觉交互式证明通过某些个体知识（可知直觉证明）的传输，在多智能体分布式系统的通信介质中实现了选言命题知识（选言可知事实）的持久传输。我们（必然）以CM为中心的证明概念也是KD 45-信念的析取显式细化，并且也产生了标准S5-知识的这种细化。单调性而非公共性是LiP、LIiP及其内在证明概念的共性。作为一个副作用，我们提供了一个简短的内在证明的析取性质的直觉主义逻辑（最初证明的哥德尔）。
2014-04-08 cs.CR cs.LO math.LO
Thoughts on sub-Turing interactive computability
本文提出可计算性逻辑的新研究方向，将无限内存等不可能具备的资源视为计算设备的外部资源，主张在表达计算问题的逻辑公式前件中明确核算这类资源，研究无需此类资源的亚图灵交互可计算性。
2024-11-03 cs.LO
ALICE: An Advanced Logic for Interactive Component Engineering
本文介绍了一个概述的验证框架ALICE在其当前版本0.7。它基于通用定理证明器Isabelle [Pau 03 a]。在ALICE中，软件或硬件组件被指定为具有定向通信信道的全状态黑盒。组件通过这些通道发送和接收异步消息。组件的行为通常被描述为一种与观察结果的关系，这种关系以流经其输入和输出通道的消息流的形式出现。支持非定时和定时以及基于状态的、递归的、关系的、等式的、假设/保证的和函数式的规格说明。因此，ALICE是非常适合的形式化和验证的分布式系统建模与此流处理范例。
2014-10-16 cs.LO cs.SE
Stit Semantics for Epistemic Notions Based on Information Disclosure in Interactive Settings
我们使用分支离散时间结构上的STIT语义来表征四种类型的代理知识。它们是\emph{ex ante}知识、\emph{ex interim}知识、\emph{ex post}知识和专有技术。前三个概念来自于对决策过程中信息披露阶段的博弈论分析，第四个概念在行动逻辑和道义逻辑中都获得了突出地位，作为一种形式化能力的手段。近年来，人工智能领域的逻辑学家认为，任何关于责任归属和罪责的全面研究都应该包括对这类知识的适当处理。本文旨在澄清以前的尝试，正式在STIT逻辑，并提出替代的解释，在我们看来，更类似于STIT传统的责任研究。我们提出的逻辑使用扩展与知识运营商的Xstit语言，公式进行评估分支离散时间模型。我们还提出了一个公理系统的逻辑，并解决其健全性和完整性。
2019-11-19 cs.LO math.LO
A program logic for union bounds
我们提出了一个基于联合界的概率霍尔逻辑aHL，这是一个来自基本概率论的工具。虽然联合界很简单，但它是分析随机算法的一个非常常用的工具。在形式化验证术语中，联合边界允许对算法可能出错的可能方式进行灵活和组合推理。它也使得关于概率的推理和关于事件的推理之间能够清晰地分离，这在我们的逻辑中被表示为标准的一阶公式。值得注意的是，我们逻辑中的断言是非概率性的，尽管我们可以从判断中得出概率性的事实。我们的逻辑还可以证明交互式程序的准确性，程序必须在输入到达时立即产生中间输出，而不是一次访问整个输入。此设置还启用自适应性，其中较晚的输入可能取决于较早的中间输出。我们展示了如何证明准确性的几个例子，从差分隐私文学，互动和非互动。
2019-11-08 cs.LO cs.PL
A Monadic Framework for Interactive Realizability
我们给出了一个新的介绍互动的可实现性与更明确的语法。交互式可实现性是一种可实现性语义，它将Curry-Howard对应扩展到（次）经典逻辑，更确切地说，扩展到一阶直觉算术（Heyting Arithmetic），该算术由排除中间法则扩展到简单的存在公式，这是一个由其在证明挖掘中的应用所激发的系统。Monad可以通过提供一种干净和模块化的方式来包含纯函数式语言中的不纯功能来构建函数式程序。我们表示交互式实现器的抽象框架，适用于一元的方法在函数式编程修改的可实现性，以获得更“宽松”的可实现性的概念，是适合于经典逻辑。特别是，我们使用的状态和异常单子的组合，以捕捉从错误中学习的交互式实现者在语法层面上的性质。
2013-10-15 cs.LO
The KB paradigm and its application to interactive configuration
KU Leuven（鲁汶大学）
知识库范式旨在以丰富的形式语言表达领域知识，并将该领域知识作为知识库，通过应用多种形式的推理来解决领域中出现的各种问题和任务。因此，该范式在信息和问题解决之间应用了严格的关注分离。在本文中，我们分析的原则和可行性的知识库范例的背景下，一类重要的应用程序：交互式配置问题。在交互式配置问题中，在约束条件下搜索相关对象的配置，其中系统帮助用户达到预期的配置。业界普遍认为，针对这些问题的良好软件解决方案非常难以开发。我们从知识库范式的角度来研究这些问题。我们表明，在这个领域中的多种功能可以通过应用不同形式的逻辑推理的配置域的正式规范。我们报告的概念证明这种方法在现实生活中的应用与银行公司。逻辑程序设计理论与实践（Theory and Practice of Logic Programming，TPLP）
2016-05-06 cs.AI cs.LO
Introduction to clarithmetic I
“Clarithmetic”是一个与皮亚诺算术类似的形式数论的通用名称，但基于可计算性逻辑（参见http：//www.cis.upenn.edu/classgi/cl.html），而不是更传统的经典或直觉逻辑。claithmetical理论的公式代表交互式计算问题，它们的“真理”被理解为算法解的存在。对这些解决方案施加各种复杂性约束会产生各种版本的clarithmetic。本文介绍了一个多项式时间可计算性的算法体系，该体系是完善的。在这个意义上，系统的每个定理T都代表一个具有多项式时间解的交互数论计算问题，而且，这样的解可以有效地从T的证明中提取出来。完备性的意义在于，每一个具有多项式时间解的交互数论问题都由系统的某个定理T表示。这篇论文是写在semitutorial风格和目标读者事先不熟悉可计算性逻辑。
2011-08-23 cs.CC cs.LO math.LO
On the system CL12 of computability logic
可计算性逻辑（参见http：//www.csc.villanova.edu/cnjaparidz/CL/）是一个长期的项目，用于在建设性游戏语义的基础上重新开发逻辑，将游戏视为交互式计算问题的抽象模型。CL 12是经典一阶逻辑的一个保守扩展，它的语言用量词和连接词的所谓选择类扩充了经典逻辑的语言。这个系统已经发现富有成效的应用程序作为皮亚诺算术的建设性和复杂性为导向的版本，如多项式时间可计算性，多项式空间可计算性，和超越算术的逻辑基础。本文介绍了第三个，必不可少的复杂性措施的互动计算称为振幅复杂性，并建立了适当的CL 12相对于A-振幅，S-空间和T-时间的可计算性在一定的最小条件下的三元组（A，S，T）的功能类。这一结果极大地拓宽了CL 12的潜在应用领域。该文件是独立的，目标读者事先不熟悉的主题。
2015-07-25 cs.LO math.LO
Computability Logic: a formal theory of interaction
可计算性逻辑是（交互式）可计算性的形式理论，就像经典逻辑是真理的形式理论一样。这种方法最近在“可计算性逻辑导论”（《纯粹与应用逻辑年鉴》123（2003），第1 -99页）中提出。本文重新介绍了可计算性逻辑在一个更紧凑和更少的技术方式。它是写在一个semitutorial风格与一般计算机科学，逻辑或数学观众铭记。关于这一主题的因特网资料可在http：//www.cis.upenn.edu/paggiorgi/cl.html上查阅，其他材料可在http://www.csc.villanova.edu/~japaridz/CL/gsoll.html上查阅。
2004-12-10 cs.AI cs.LO math.LO
Many concepts and two logics of algorithmic reduction
在为可计算性逻辑的各个部分寻找公理化的程序中，早先证明了交互式图灵归约逻辑正是海廷直觉主义演算的蕴涵片段。这种简化允许对前件所表示的计算资源进行无限的重用。然而，一种至少同样基本和自然的算法简化是不允许这种重用的。本文表明，把第一类归约的逻辑转变为第二类归约的逻辑，只需要从它的根岑式公理化中删除收缩规则。第一种（图灵）交互式约简也有三种自然版本。虽然这三个版本彼此非常不同，但它们的逻辑行为（孤立地）是无法区分的，而这种共同行为被隐含的直觉主义逻辑精确地捕获。在本文的其他贡献是一个非正式的介绍了一系列新的-有限和有界-版本的递归操作和相关的减少操作。有关可计算性逻辑的在线资源可在http://www.cis.upenn.edu/~giorgi/cl.html上找到
2008-10-12 cs.LO math.LO
The intuitionistic fragment of computability logic at the propositional level
从可计算性逻辑的语义出发，给出命题直觉演算的可靠性和完备性证明。后者将公式解释为交互式计算问题，形式化为机器与其环境之间的游戏。直觉主义蕴涵被理解为在最弱的可能性-因此最自然-意义上的算法还原，析取和合取作为问题的确定性选择组合（析取=机器的选择，合取=环境的选择），而“荒谬”作为普遍力量的计算问题。请访问http://www.cis.upenn.edu/~giorgi/cl.html以获得关于可计算性逻辑的全面在线资源。
2006-02-11 cs.AI cs.LO math.LO
An Environment for the Exploration of Non Monotonic Logic Programs
稳定模型语义和良好基础语义已经被证明是非常有用的几个应用程序的非单调推理。然而，稳定模型呈现高计算复杂性，而良好基础语义易于计算并且提供稳定模型的近似。对于逻辑程序的两种语义都存在有效的引擎。这项工作提出了两个这样的系统，即XSB和SMODELS的计算集成。由此产生的系统被称为XNMR，并提供了一个交互式的系统，用于探索这两种语义。模块化等方面可以利用，以方便调试大型知识库与通常的Prolog调试技术和交互式环境。此外，使用完整的Prolog系统作为Stable Models引擎的前端，增强了此类系统通常接受的语言。
2001-11-19 cs.LO cs.PL
From truth to computability II
可计算性逻辑是关于计算任务和资源的形式化理论。其中的公式代表交互式计算问题，而“真理”被理解为算法的可解性。交互式计算问题，反过来，被定义为某种类型的游戏之间的机器和它的环境，与逻辑运算符代表这种游戏的操作。在为这个语义引入逻辑的增量丰富片段寻找公理化的雄心勃勃的计划中，早期的文章“从真理到可计算性I”证明了系统CL3的可靠性和完备性，其语言具有所谓的平行连接词（包括否定），选择连接词，选择量词和盲量词。本文将这一结果扩展到具有相同逻辑运算符集合的更具表现力的系统CL4。使CL4富有表现力的是在其语言中存在两种原子：基本原子，代表基本计算问题（即谓词，即零交互度的问题），和一般原子，代表任意计算问题。CL4保守地扩展了CL3，后者只是前者的一般无原子片段。从CL4语言中删除盲（经典）量词组，产生一个可判定的逻辑，尽管后者仍然是一阶的。有关可计算性逻辑的全面在线资源可以在http://www.cis.upenn.edu/~giorgi/cl.html上找到
2005-07-20 cs.AI cs.LO math.LO
From truth to computability I
可计算性逻辑是最近提出的一种交互计算的形式化理论。有关该主题的全面在线资源，请访问http://www.cis.upenn.edu/~giorgi/cl.html。本文包含了一个合理性和完整性证明的演绎系统CL3公理化的最基本的一阶片段的可计算性逻辑称为有限深度，元素基片段。这一结果的潜在应用领域包括交互计算理论、建设性应用理论、知识库系统、资源约束规划和行动系统。本文件是自成一体的，因为它重新介绍了所有相关定义以及主要动机。
2005-07-20 cs.AI cs.GT cs.LO
In the beginning was game semantics
本文概述了可计算性逻辑--交互式计算任务和资源的游戏语义构造逻辑。只有一个非概述，在它的技术部分，致力于证明健全的仿射逻辑方面的语义可计算性逻辑。有关该主题的全面在线资源可以在http://www.cis.upenn.edu/~giorgi/cl.html上找到
2008-10-24 cs.AI cs.LO math.LO
CryptoVampire: Automated Reasoning for the Complete Symbolic Attacker Cryptographic Model
本文提出 CryptoVampire，首次通过一阶形式化、子项关系处理及 Vampire 饱和推理，全自动完成 BC Logic 中密码协议轨迹属性证明。
2024-04-05 cs.CR cs.LO
Isabelle: The Next 700 Theorem Provers
Isabelle是一个通用的定理证明器，设计用于各种形式理论的交互式推理。目前，它为构造类型论、各种一阶逻辑、Zermelo-Fraenkel集合论和高阶逻辑提供了有用的证明过程。这一调查伊莎贝尔作为一个介绍文学。它解释了为什么一般的定理证明是有益的。它提供了一个彻底的历史伊莎贝尔，从它的起源在LCF系统。它提出了一个帐户的逻辑是如何表示，说明使用经典逻辑。该方法与爱丁堡逻辑框架进行了比较。几个伊莎贝尔对象逻辑。
2000-10-31 cs.LO
Implementing program extraction from CL1-proofs
可计算性逻辑（Computability Logic，CoL）是一种交互计算的形式化理论。它将计算问题理解为两个玩家的游戏：机器和它的环境，使用逻辑形式主义来描述有效的可计算性原则和公式来表示计算问题。逻辑CL1是CoL的一个片段的演绎系统，逻辑词汇表包含了经典逻辑的所有算子和选择算子，原子表示经典逻辑的基本博弈即谓词。在本文中，我们提出了一个程序，采取CL1证明的任意公式$F$，并提取一个获胜的策略，$F$从证明，然后发挥$F$使用该策略。我们希望本文将提供一个起点，进一步的工作，在程序提取的CoL为基础的算法和其他CoL为基础的应用系统。
2013-11-26 cs.LO
Interpreting a Classical Geometric Proof with Interactive Realizability
我们展示了如何提取一个单调的学习算法从一个经典的几何语句的证明，通过解释的证明，通过交互式可实现性，可实现语义的经典逻辑。该陈述是关于包含实平面中的有限点集的凸角的存在性，并且它与凸包的存在性有关。我们将实数定义为有理数的柯西序列，因此等式和排序是不可判定的。虽然证明表面上看起来是建设性的，但它使用经典推理来处理实数之间的不可判定比较，使得底层算法无效。交互式可实现性解释将证明所描述的非有效线性算法转换为使用回溯从错误中学习的有效算法。有效的算法表现出“智能”的行为，只执行证明最终语句所需的精度的比较。这种行为并没有明确的计划，但产生于柯西序列之间的比较的交互式解释。
2013-09-05 cs.CG cs.LO
Propositional Computability Logic II
可计算性逻辑是关于计算任务和资源的形式化理论。它的公式代表交互式计算问题，逻辑运算符代表计算问题的运算，公式的有效性被理解为总是有算法解决方案的问题的方案。关于这一主题的全面在线资源可在http://www.cis.upenn.edu/~giorgi/cl.html上查阅。早期的文章“命题可计算性逻辑I”证明了可计算性逻辑的最小非平凡片段CL1的可靠性和完备性。本文将这一结果扩展到更有表现力的命题系统CL2。使CL2比CL1更具表达力的是其语言中存在两种原子：基本原子，表示基本计算问题（即谓词），以及一般原子，表示任意计算问题。CL2保守地扩展了CL1，后者只是前者的一般无原子片段。
2004-06-20 cs.GT cs.LO math.LO
Propositional computability logic I
与经典逻辑是真的形式理论一样，最近提出的可计算性逻辑也是可计算性的形式理论。它将（交互式）计算问题理解为机器与环境的博弈，将其可计算性理解为总是赢得博弈的机器的存在，将逻辑运算符理解为计算问题的运算，将逻辑公式的有效性理解为“总是可计算”问题的方案。目前的贡献给出了一个最基本的片段的可计算性逻辑的公理化的合理性和完整性证明的详细阐述。这个片段的逻辑词汇表包含所谓的并行和选择操作的操作符，它的原子代表基本问题，即标准意义上的谓词。这篇文章是自成一体的，因为它解释了所有相关的概念。虽然在技术上没有必要，但是，熟悉基础论文“Introduction to computability logic”[Annals of Pure and Applied Logic 123（2003），pp.1-99]将极大地帮助读者理解可计算性逻辑的哲学，潜在的动机，潜力和实用性，--决定当前结果价值的背景。有关该主题的在线介绍可在http://www.cis.upenn.edu/~giorgi/cl.html和http://www.csc.villanova.edu/~japaridz/CL/gsoll.html上查阅。
2004-06-21 cs.LO math.LO
Interactive Formal Specification for Mathematical Problems of Engineers
本文作为ISAC项目原型系统描述的第二部分，介绍无需逻辑知识即可交互构建形式化规约的规约阶段设计与实现，推广形式化框架的复用，适用于工程教育与高中场景。
2024-04-08 cs.HC cs.LO
