Unification in pseudo-linear sort theories is decidable

DOI10.1007/3-540-61511-3_99zbMath1415.03033OpenAlexW1562994860MaRDI QIDQ4647533

Christoph Weidenbach

Publication date: 15 January 2019

Published in: Automated Deduction — Cade-13 (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/3-540-61511-3_99

zbMATH Keywords

unification problemtree automatondecidability resultground termfunction symbol

Mathematics Subject Classification ID

Automata and formal grammars in connection with logical questions (03D05) Decidability of theories and sets of sentences (03B25) Mechanization of proofs and logical operations (03B35)

Cites Work

• Unification theory
• Unification in sort theories and its applications
• Computational aspects of an order-sorted logic with term declarations
• Pumping, cleaning and symbolic constraints solving
• Inductive proofs by specification transformations
• Equality and disequality constraints on direct subterms in tree automata
• Unnamed Item
• Unnamed Item

This page was built for publication: Unification in pseudo-linear sort theories is decidable