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

17th Conference on Computability in Europe (CiE)

作者： Koutsoukou-Argyraki, Angeliki Univ Cambridge Dept Comp Sci & Technol Comp Lab Cambridge England

ISBN: (纸本)9783030800499;9783030800482

Instead of using program extraction mechanisms in various theorem provers, I suggest that users opt to create a database of formal proofs whose computational content is made explicit;this would be an alternative approach which, as libraries of formal mathematical proofs are constantly growing, would rely on future advances in automation and machine learning tools, so that as blocks of (sub)proofs get generated automatically, the preserved computational content would get recycled, recombined and would eventually manifest itself in different contexts. To this end, I do not suggest restricting to only constructive proofs, but I suggest that proof mined, possibly also non-constructive proofs with some explicit computational content should be preferable, if possible. To illustrate what kind of computational content in mathematical proofs may be of interest I give several very elementary examples (to be regarded as building blocks of proofs) and some samples of formalisations in Isabelle/HOL. Given the state of the art in automation and machine learning tools currently available for proof assistants, my suggestion is rather speculative, yet starting to build a database of formal proofs with explicit computational content would be a potentially useful first step.

关键词： Proof assistants computational content Proof mining Isabelle/HOL Proof theory Interactive theorem provers Formalisation Machine learning

来源：评论

学校读者我要写书评

暂无评论

The Jacobson radical for an inconsistency predicate

引用

COMPUTABILITY-THE JOURNAL OF THE ASSOCIATION CIE 2022年第2期11卷 147-162页

作者： Schuster, Peter Wessel, Daniel Univ Verona Dipartimento Informat Verona Italy

As a form of the Axiom of Choice about relatively simple structures (posets), Hausdorff's Maximal Chain Principle appears to be little amenable to computational interpretation. This received view, however, requires revision: maximal chains are more reminiscent of maximal ideals than it seems at first glance. The latter live in richer algebraic structures (rings), and thus are readier to be put under computational scrutiny. Exploiting this, and of course the analogy between maximal chains and maximal ideals, the concept of Jacobson radical carries over from a ring to an arbitrary set with an abstract inconsistency predicate: that is, a distinguished monotone family of finite subsets. All this makes possible not only to generalise Hausdorff's principle, but also to express it as a syntactical conservation theorem. The latter, which encompasses the desired computational core of Hausdorff's principle, is obtained by a generalised inductive definition. The over-all setting is constructive set theory.

关键词： Axiom of choice maximal chain maximal ideal consistent theory Jacobson radical syntactical conservation computational content constructive set theory inductive definition finite binary tree

来源：评论

学校读者我要写书评

暂无评论

Herbrand schemes for cyclic proofs

引用

JOURNAL OF LOGIC AND COMPUTATION 2025年第4期35卷

作者： Afshari, Bahareh Enqvist, Sebastian Leigh, Graham E. Univ Gothenburg Dept Philosophy Linguist & Theory Sci S-40530 Gothenburg Sweden Stockholm Univ Dept Philosophy S-10691 Stockholm Sweden

Recent work by Afshari et al. introduces a notion of Herbrand schemes for first-order logic by associating a higher-order recursion scheme to a sequent calculus proof. Calculating the language of associated Herbrand schemes directly yields Herbrand disjunctions. As such, these schemes can be seen as programs extracted from proofs. The present article generalizes this computational interpretation by removing the restriction of acyclicity from Herbrand schemes which amounts to admitting recursively defined programs. It is shown that the notion of proof corresponding to these generalized Herbrand schemes is cyclic proofs, considered here in the context of classical theories of inductively defined predicates. In particular, for cyclic proofs of generalized Sigma(1)-sequents, Herbrand schemes extract sets of witnessing terms via a simulation of non-wellfounded cut elimination.

关键词： Sequent Calculus Inductive Definitions Cyclic and non-Wellfounded Proofs Herbrand's Theorem Cut Elimination Multicut Higher-order Recursion Schemes computational content

来源：评论

学校读者我要写书评

暂无评论

Herbrand schemes for first-order logic

引用

ARCHIVE FOR MATHEMATICAL LOGIC 2025年 1-70页

作者： Afshari, Bahareh Enqvist, Sebastian Leigh, Graham E. Univ Gothenburg Dept Philosophy Linguist & Theory Sci Gothenburg Sweden Stockholm Univ Dept Philosophy Stockholm Sweden

This article provides a language-theoretic rendering of Herbrand's theorem. To each first-order proof is associated a higher-order recursion scheme that abstracts the computation of Herbrand sets obtained through Gentzen-style multicut elimination. The representation extends previous results in this area by lifting the prenex restriction on cut formulas and relaxing the cut-elimination strategies. Features of the new approach are the interpretation of cut as simple composition and contraction as 'call with current continuation'.

关键词： Sequent Calculus First-order Logic Herbrand's Theorem Cut Elimination Multicut Higher-order Recursion Schemes computational content

来源：评论

学校读者我要写书评

暂无评论

Radical theory of Scott-open filters

引用

THEORETICAL COMPUTER SCIENCE 2023年第1期945卷

作者： Misselbeck-Wessel, Daniel Schuster, Peter Univ Verona Dipartimento Informat Str Grazie 15 I-37134 Verona Italy

Following the Kronecker-Duval or D5 philosophy of dynamic evaluation in computer algebra, the dynamical proof method was brought into constructive algebra in order to obtain computational interpretations of the individual, concrete instances of the Kuratowski-Zorn Lemma modern algebra abounds with. We now push this approach into complete lattices, and thus capture the computational content also of generic, abstract forms of the axiom of choice such as the Teichmuller-Tukey lemma. To this end we first strengthen the (key lemma for) the Hofmann-Mislove theorem about Scott-open filters (SOF): to be a member of a SOF is equivalent, with the axiom of choice, to membership of all complete extensions. This then allows for a constructive treatment: membership of the given SOF means that from the potential element one can grow a finite labelled binary tree of an inductively defined type such that every branch of the tree eventually dips into the SOF. The ideal objects characteristic for invocations of the Kuratowski-Zorn Lemma are thus approximated and actually replaced by paths in those trees, by which we shed light on the interaction of transfinite methods and their dynamical interpretation. The first test case includes abstract dependence, especially bases of vector spaces. Key to the above lies in taking Erne's saturation map as a radical operator for Scott-open sets. Through a generalised inductive definition this radical can be pinned down in terms of universal properties;and reaches into classical pointfree topology, as exemplified by a succinct proof of Isbell's spatiality theorem. (c) 2022 Elsevier B.V. All rights reserved.

关键词： Dynamical proof Complete lattice Scott -open filter Nucleus Hofmann-Mislove theorem Isbell?s spatiality theorem Axiom of choice Teichm?ller-Tukey lemma Syntax from semantics computational content Constructive algebra Finite binary tree Inductive definition

来源：评论

学校读者我要写书评

暂无评论

引用

JMIR PUBLIC HEALTH AND SURVEILLANCE 2021年第11期7卷 e26660页

作者： Chang, Angela Schulz, Peter Johannes Jiao, Wen Liu, Matthew Tingchi Univ Macau Fac Social Sci E21 FSS Bldg2nd Fl Taipa 100 Macao Peoples R China Univ Lugano Inst Commun & Hlth Lugano Switzerland Univ Macau Fac Business Adm Taipa Macao Peoples R China

Background: The fact that the number of individuals with obesity has increased worldwide calls into question media efforts for informing the public. This study attempts to determine the ways in which the mainstream digital news covers the etiology of obesity and diseases associated with the burden of obesity. Objective: The dual objectives of this study are to obtain an understanding of what the news reports on obesity and to explore meaning in data by extending the preconceived grounded theory. Methods: The 10 years of news text from 2010 to 2019 compared the development of obesity-related coverage and its potential impact on its perception in Mainland China, Hong Kong, and Taiwan. Digital news stories on obesity along with affliction and inferences in 9 Chinese mainstream newspapers were sampled. An automatic content analysis tool, DiVoMiner was proposed. This computer-aided platform is designed to organize and filter large sets of data on the basis of the patterns of word occurrence and term discovery. Another programming language, Python 3, was used to explore connections and patterns created by the Results: A total of 30,968 news stories were identified with increasing attention since 2016. The highest intensity of newspaper coverage of obesity communication was observed in Taiwan. Overall, a stronger focus on 2 shared causative attributes of obesity is on stress (n=4483, 33.0%) and tobacco use (n=3148, 23.2%). The burdens of obesity and cardiovascular diseases are implied to be the most, despite the aggregated interaction of edge centrality showing the highest link between the "cancer" and obesity. This study goes beyond traditional journalism studies by extending the framework of computational and customizable web-based text analysis. This could set a norm for researchers and practitioners who work on data projects largely for an innovative attempt. Conclusions: Similar to previous studies, the discourse between the obesity epidemic and personal afflictions i

关键词： public health computational content digital research methods obesity discourse gene disorders noncommunicable disease

来源：评论

学校读者我要写书评

暂无评论

Reverse formalism 16

引用

SYNTHESE 2020年第2期197卷 497-544页

作者： Sanders, Sam Ludwig Maximilians Univ Munchen Munich Ctr Math Philosophy Munich Germany Univ Ghent Dept Math Ghent Belgium

In his remarkable paper Formalism 64, Robinson defends his eponymous position concerning the foundations of mathematics, as follows: Any mention of infinite totalities is literally meaningless. We should act as if infinite totalities really existed. Being the originator of Nonstandard Analysis, it stands to reason that Robinson would have often been faced with the opposing position that 'some infinite totalities are more meaningful than others', the textbook example being that of infinitesimals (versus less controversial infinite totalities). For instance, Bishop and Connes have made such claims regarding infinitesimals, and Nonstandard Analysis in general, going as far as calling the latter respectively a debasement of meaning and virtual, while accepting as meaningful other infinite totalities and the associated mathematical framework. We shall study the critique of Nonstandard Analysis by Bishop and Connes, and observe that these authors equate 'meaning' and 'computational content', though their interpretations of said content vary. As we will see, Bishop and Connes claim that the presence of ideal objects (in particular infinitesimals) in Nonstandard Analysis yields the absence of meaning (i.e. computational content). We will debunk the Bishop-Connes critique by establishing the contrary, namely that the presence of ideal objects (in particular infinitesimals) in Nonstandard Analysis yields the ubiquitous presence of computational content. In particular, infinitesimals provide an elegant shorthand for expressing computational content. To this end, we introduce a direct translation between a large class of theorems of Nonstandard Analysis and theorems rich in computational content (not involving Nonstandard Analysis), similar to the 'reversals' from the foundational program Reverse Mathematics. The latter also plays an important role in gauging the scope of this translation.

关键词： Abraham Robinson Formalism Nonstandard analysis computational content

来源：评论

学校读者我要写书评

暂无评论

The computational Significance of Hausdorff's Maximal Chain Principle 16th

The Computational Significance of Hausdorff's Maximal Chain ...

引用

16th Conference on Computability in Europe (CiE)

作者： Schuster, Peter Wessel, Daniel Univ Verona Dipartimento Informat Str Grazie 15 I-37134 Verona Italy

ISBN: (纸本)9783030514662;9783030514655

As a fairly frequent form of the Axiom of Choice about relatively simple structures (posets), Hausdorff's Maximal Chain Principle appears to be little amenable to computational interpretation. This received view, however, requires revision. When attempting to convert Hausdorff's principle into a conservation theorem, we have indeed found out that maximal chains are more reminiscent of maximal ideals than it might seem at first glance. The latter live in richer algebraic structures (rings), and thus are readier to be put under computational scrutiny. Exploiting the newly discovered analogy between maximal chains and ideals, we can carry over the concept of Jacobson radical from a ring to an arbitrary set with an irreflexive symmetric relation. This achievement enables us to present a generalisation of Hausdorff's principle first as a semantic and then as a syntactical conservation theorem. We obtain the latter, which is nothing but the desired computational core of Hausdorff's principle, by passing from maximal chains to paths of finite binary trees of an adequate inductively generated class. In addition to Hausdorff's principle, applications include the Maximal Clique Principle for undirected graphs. Throughout the paper we work within constructive set theory.

关键词： Axiom of Choice Maximal chain Maximal ideal Maximal clique Jacobson radical Proof-theoretic conservation computational content Constructive set theory Finite binary tree Inductive generation

来源：评论

学校读者我要写书评

暂无评论

Resolving finite indeterminacy A definitive constructive universal prime ideal theorem 20

Resolving finite indeterminacy A definitive constructive uni...

引用

35th Annual ACM/IEEE Symposium on Logic in Computer Science (LICS)

作者： Schuster, Peter Wessel, Daniel Univ Verona Dipartimento Informat Verona Italy

ISBN: (纸本)9781450371049

Dynamical methods were designed to eliminate the ideal objects abstract algebra abounds with. Typically granted by an incarnation of Zorn's Lemma, those ideal objects often serve for proving the semantic conservation of additional non-deterministic sequents, that is, with finite but not necessarily singleton succedents. Eliminating ideal objects dynamically was possible also because (finitary) coherent or geometric logic predominates in that area: the use of a nondeterministic axiom can be captured by a finite branching of the proof tree. Incidentally, a paradigmatic case has widely been neglected in dynamical algebra: Krull's Lemma for prime ideals. Digging deeper just about that case, which we have dealt with only recently (with Yengui), has now brought us to unearth the general phenomenon underlying dynamical algebra: Given a claim of computational nature that usually is proved by the semantic conservation of certain additional non-deterministic axioms, there is a finite labelled tree belonging to a suitable inductively generated class which tree encodes the desired computation. Our characterisation works in the fairly universal setting of a consequence relation enriched with non-deterministic axioms;uniformises many of the known instances of the dynamical method;generalises the proof-theoretic conservation criterion we have offered before (with Rinaldi);and last but not least links the syntactical with the semantic approach: every ideal object used for the customary proof of a concrete claim can be approximated by one of the corresponding tree's branches.

关键词： dynamical proof non-deterministic axiom geometric logic proof-theoretic conservation finite tree computational content inductive generation Krull's Lemma prime ideals

来源：评论

学校读者我要写书评

暂无评论

Herbrand's theorem as higher order recursion

引用

ANNALS OF PURE AND APPLIED LOGIC 2020年第6期171卷 102792-102792页

作者： Afshari, Bahareh Hetzl, Stefan Leigh, Graham E. Univ Amsterdam Inst Log Language & Computat POB 94242 NL-1090 GE Amsterdam Netherlands Univ Gothenburg Dept Philosophy Linguist & Theory Sci Box 200 S-40530 Gothenburg Sweden TU Wien Inst Diskrete Math & Geometrie Wiedner Hauptstr 8-10 A-1040 Vienna Austria

This article examines the computational content of the classical Gentzen sequent calculus. There are a number of well-known methods that extract computational content from first-order logic but applying these to the sequent calculus involves first translating proofs into other formalisms, Hilbert calculi or Natural Deduction for example. A direct approach which mirrors the symmetry inherent in sequent calculus has potential merits in relation to proof-theoretic considerations such as the (non-)confluence of cut elimination, the problem of cut introduction, proof compression and proof equivalence. Motivated by such applications, we provide a representation of sequent calculus proofs as higher order recursion schemes. Our approach associates to an LK proof pi of double right arrow there exists nu F, where F is quantifier free, an acyclic higher order recursion scheme H with a finite language yielding a Herbrand disjunction for there exists nu F. More generally, we show that the language of H contains all Herbrand disjunctions computable from pi via a broad range of cut elimination strategies. (C) 2020 The Authors. Published by Elsevier B.V.

关键词： Classical sequent calculus Herbrand's theorem Cut elimination Higher order recursion schemes computational content

来源：评论

学校读者我要写书评

暂无评论

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

时间限定

文献类型

馆藏选择

核心期刊

语言

文献类型

帮助

文字说明：

检索规则说明：

检索范例：

分类表

所选分类

限定检索结果

文献类型

馆藏范围

日期分布

学科分类号

主题

机构

作者

语言

请选择保存的检索档案：

请选择收藏分类：

通借通还

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

时间限定

文献类型

馆藏选择

核心期刊

语言

文献类型

帮助

文字说明：

检索规则说明：

检索范例：

分类表

所选分类

限定检索结果

文献类型

馆藏范围

日期分布

学科分类号

主题

机构

作者

语言

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

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

通借通还

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

请选择保存的检索档案：

请选择收藏分类：