Refinement of bounds of the height of terms in the most general unifier

DOI10.1007/BF02362269zbMath0946.03015OpenAlexW2043539723MaRDI QIDQ1977922

B. Yu. Konev

Publication date: 6 June 2000

Published in: Journal of Mathematical Sciences (New York) (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/bf02362269

zbMATH Keywords

most general unifierdepth differencelower bound for the heights of termsproofs in Gentzen-type sequential calculiupper bounds of the heights of terms

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35) Complexity of proofs (03F20)

Cites Work

• The number of proof lines and the size of proofs in first order logic
• Linear unification
• Proof schemata in Hilbert-type axiomatic theories
• Unnamed Item

This page was built for publication: Refinement of bounds of the height of terms in the most general unifier