×

zbMATH — the first resource for mathematics

On a unification problem related to Kreisel’s conjecture. (English) Zbl 0664.03037
M. Baaz (Wien) hat (bisher unpublizierte) Fortschritte bei bekannten Problemen aus Beweistheorie und Informatik dadurch erzielt, daß er diese auf das folgende einstufige Unifizierung-Matching-Problem zurückführt:
(UM) Existieren zu gegebenen Termpaaren \(s_ 1,t_ 1;...;s_ n,t_ n\) Substitutionen \(\delta,\sigma_ 1,...,\sigma_ n\) mit \(s_ i\delta \sigma_ i=t_ i\delta:\) \(1\leq i\leq n?\)
Baaz zeigt: Hat (UM) eine Lösung, so auch eine mit allgemeinstem \(\delta\). - Diese Note enthält dazu weitere Resultate:
a) (UM) kann effektiv auf (UM) mit \(n=2\) zurückgeführt werden.
b) (UM) ist für \(n=1\) entscheidbar. Bei positiver Entscheidung liefert der Algorithmus das Resultat von Baaz. Einige irreführende Druckfehler werden in einem Corrigendum (mit weiteren Informationen) berichtigt, das der Verfasser demnächst herausgeben wird.
Reviewer: H.Luckhardt

MSC:
03F99 Proof theory and constructive mathematics
68T15 Theorem proving (deduction, resolution, etc.) (MSC2010)
03B35 Mechanization of proofs and logical operations
PDF BibTeX XML Cite
Full Text: EuDML