First-Order Schemata and Inductive Proof Analysis
暫譯: 一階模式與歸納證明分析

Leitsch, Alexander, Cerna, David Michael, Lolic, Anela

First-Order Schemata and Inductive Proof Analysis
  • 出版商: Springer
  • 出版日期: 2026-01-03
  • 售價: $7,340
  • 貴賓價: 9.5 折 $6,973
  • 語言: 英文
  • 頁數: 246
  • 裝訂: Hardcover - also called cloth, retail trade, or trade
  • ISBN: 303205740X
  • ISBN-13: 9783032057402
  • 相關分類: Computer-Science

    • 海外代購書籍(需單獨結帳)

相關主題

商品描述

Schemata are formal tools for describing inductive reasoning. They opened a new area in the analysis of inductive proofs.

The book introduces schemata for first-order terms, first-order formulas and first-order inference systems. Based on general first-order schemata, the cut-elimination-by-resolution (CERES) method--developed around the year 2000--is extended to schematic proofs. This extension requires the development of schematic methods for resolution and unification which are defined in this book. The added value of proof schemata compared to other inductive approaches consists in the extension of Herbrand's theorem to inductive proofs (in the form of Herbrand systems, which can be constructed effectively). An application to an analysis of mathematical proof is given. The work also contains and extends the newest results on schematic unification and corresponding algorithms.

Core topics covered:

  • first-order schemata
  • cut-elimination by resolution
  • point transition systems
  • schematic resolution
  • Herbrand systems
  • inductive proof analysis

This volume is the first comprehensive work on first-order schemata and their applications. As such, it will be eminently suitable for researchers and PhD students in logic and computer science either working or with an interest in proof theory, inductive reasoning and automated deduction. Prerequisites are a firm knowledge of first-order logic, basic knowledge of automated deduction and a background in theoretical computer science.

Alexander Leitsch and Anela Lolic are affiliated with the Institute of Logic and Computation of the Technische Universität Wien, David M. Cerna with the Czech Academy of Sciences, Institute of Computer Science (Ústav informatiky AV ČR, v.v.i.).

商品描述(中文翻譯)

Schemata 是描述歸納推理的正式工具。它們在歸納證明的分析中開啟了一個新領域。

本書介紹了針對一階術語、一階公式和一階推理系統的 schemata。基於一般的一階 schemata，切割消除法（cut-elimination-by-resolution, CERES）——於2000年左右發展——被擴展到 schemata 證明。這一擴展需要開發針對解析和統一的 schemata 方法，這些方法在本書中有定義。與其他歸納方法相比，證明 schemata 的附加價值在於將 Herbrand 定理擴展到歸納證明（以 Herbrand 系統的形式，這些系統可以有效構建）。本書還提供了對數學證明分析的應用。該工作還包含並擴展了有關 schemata 統一及相應算法的最新結果。

核心主題包括：
- 一階 schemata
- 通過解析的切割消除
- 點轉換系統
- schemata 解析
- Herbrand 系統
- 歸納證明分析

本卷是關於一階 schemata 及其應用的第一部綜合性著作。因此，它將非常適合在邏輯和計算機科學領域從事或對證明理論、歸納推理和自動推理感興趣的研究人員和博士生。先決條件是對一階邏輯有堅實的知識，對自動推理有基本的了解，以及理論計算機科學的背景。

Alexander Leitsch 和 Anela Lolic 隸屬於維也納科技大學邏輯與計算研究所，David M. Cerna 則隸屬於捷克科學院計算機科學研究所（Ústav informatiky AV ČR, v.v.i.）。

作者簡介

David Cerna is a computational logician who has held positions at several research institutions including Czech Academy of Sciences, Dynatrace Research, and the Research Institute for Symbolic Computation. In 2015, he earned his PhD from the Technical University of Vienna in the field of computational proof theory. He has expertise in the areas of Inductive Synthesis, Unification Theory, and automated reasoning.

Alexander Leitsch is retired professor of Mathematics and Theoretical Computer Science at the Technische Universität Wien. His main research areas are Computational Logic, Proof Theory and Automated Deduction. He is author of the book The Resolution calculus (Springer 1997) and of the book Methods of Cut-Elimination with coauthor Matthias Baaz (Springer 2011). He was the head of the Theory and Logic group in the Institute of Logic and Computation and the leader of seven research projects in various areas of Computational Logic supported by the Austrian Science Fund.

Anela Lolic is a logician at the Institute of Logic and Computation, TU Wien, specializing in structural proof theory. She earned her PhD in Computer Science from TU Wien in 2020, with a thesis focused on the CERES method for automated proof analysis. As principal investigator and researcher, she leads projects such as PANDAFOREST ("Proof analysis and automated deduction for recursive structures") and on Skolemization and Interpolation, supported by the Austrian Science Fund FWF and the Austrian Academy of Sciences.

作者簡介(中文翻譯)

大衛·切爾納是一位計算邏輯學家，曾在多個研究機構任職，包括捷克科學院、Dynatrace Research以及符號計算研究所。2015年，他在維也納科技大學獲得計算證明理論領域的博士學位。他在歸納合成、統一理論和自動推理等領域擁有專業知識。 亞歷山大·萊奇是維也納科技大學數學與理論計算機科學的退休教授。他的主要研究領域包括計算邏輯、證明理論和自動推理。他是書籍《解析計算》（Springer 1997）的作者，以及與合著者馬提亞斯·巴茲共同撰寫的《切除方法》（Springer 2011）的作者。他曾擔任邏輯與計算研究所的理論與邏輯小組負責人，並領導七個由奧地利科學基金支持的計算邏輯各領域的研究項目。 安內拉·洛利克是維也納科技大學邏輯與計算研究所的邏輯學家，專注於結構證明理論。她於2020年在維也納科技大學獲得計算機科學博士學位，論文專注於自動證明分析的CERES方法。作為主要研究者和研究員，她領導的項目包括PANDAFOREST（「遞歸結構的證明分析和自動推理」）以及斯科倫化和插值的研究，這些項目均由奧地利科學基金FWF和奧地利科學院支持。

類似商品