Artin Approximation, Arc-Räume, Auflösung von Singularitäten

@techreport{RISC5549,
author = {Alexander Baumgartner and Temur Kutsia and Jordi Levy and Mateu Villaret},
title = {{Term-Graph Anti-Unification}},
language = {english},
number = {18-02},
year = {2018},
length = {19},
type = {RISC Report Series},
institution = {Research Institute for Symbolic Computation (RISC), Johannes Kepler University Linz},
address = {Schloss Hagenberg, 4232 Hagenberg, Austria}
}

@techreport{RISC5594,
author = {David M. Cerna},
title = {{A General Recursive Construction for Schematic Resolution Derivations}},
language = {english},
abstract = {Proof schemata provide an alternative formalism for handling inductive argumentation, while non-trivially extending {\em Herbrand's theorem} to a fragment of arithmetic and thus allowing the construction of {\em Herbrand sequents} and {\em expansion trees}. Existing proof analysis methods for proof schemata extract an unsatisfiable characteristic formula representing the cut structure of the proof and from its refutation construct a Herbrand sequent. Unfortunately, constructing the refutation is a task which is highly non-trivial. An automated method for constructing such refutations exists, but it only works for a very weak fragment of arithmetic and is hard to use interactively. More expressive yet interactive methods for the formalization of recursive resolution refutation are complex, hard to work with, and still limited to an undesirably weak class of recursion. In this work we note a particular problem with previous methods, namely they mix the recursive structure with the calculus of refutation. Also we present a modular recursive structure independent of the resolution formalism and proof construction. We illustrate the expressive power of the so called {\em finite saturated tree} formalism by formalizing the Non-injectivity Assertion's schematic refutation (a variant of the infinitary Pigeonhole principle). None of the previously developed formalism are able to formalize this refutation.},
year = {2018},
note = {submitted for review},
length = {42},
type = {Preprint},
type = {RISC Report Series},
institution = {Research Institute for Symbolic Computation (RISC), Johannes Kepler University Linz},
address = {Schloss Hagenberg, 4232 Hagenberg, Austria}
}