Sequoia: A Playground for Logicians
Sequoia: A Playground for Logicians
复制标题
红杉：逻辑学家的游乐场
DOI：
--
复制
发表时间：
2020
期刊：
影响因子：
--
通讯作者：
Mohammed Hashim
中科院分区：
文献类型：
--
作者：
Giselle Reis;Zan Naeem;Mohammed Hashim
由于逻辑中的规则、证明和元性质证明的规律性，序贯演算是一种研究逻辑和逻辑性质的普遍技术。然而，即使是简单的证明也可能很大，而且手写往往很混乱。此外，微积分的组合性质使人们很容易犯错误或遗漏情况。红杉旨在缓解这些问题。Sequoia是一个基于web的应用程序，用于指定顺序演算并执行关于它们的基本推理。目标是成为一个用户友好的程序，逻辑学家可以指定和“玩”他们的演算。为此，我们提供了一个直观的界面，可以在其中输入推理规则，并立即使用相应的符号呈现。然后，用户可以按照他们定义的任何一种演算方法，以一种简化的、最省力的方式构建证明树。除此之外，我们还提供了一些最重要的元理论性质的检查，例如弱化可接受性和身份扩展，因为它们是通过通常的结构归纳进行的。从这个意义上说，逻辑学家只剩下每个分析中最棘手和最有趣的情况。
Sequent calculus is a pervasive technique for studying logics and their properties due to the regularity of rules, proofs, and meta-property proofs across logics. However, even simple proofs can be large, and writing them by hand is often messy. Moreover, the combinatorial nature of the calculus makes it easy for humans to make mistakes or miss cases. Sequoia aims to alleviate these problems. Sequoia is a web-based application for specifying sequent calculi and performing basic reasoning about them. The goal is to be a user-friendly program, where logicians can specify and “play” with their calculi. For that purpose, we provide an intuitive interface where inference rules can be input in and are immediately rendered with the corresponding symbols. Users can then build proof trees in a streamlined and minimal-effort way, in whichever calculus they defined. In addition to that, we provide checks for some of the most important meta-theoretical properties, such as weakening admissibility and identity expansion, given that they proceed by the usual structural induction. In this sense, the logician is only left with the tricky and most interesting cases of each analysis.