Unification in pseudo-linear sort theories is decidable

DOI10.1007/3-540-61511-3_99MaRDI QIDQ4647533zbMATH OpenOpenAlexFDO

Authors 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

decidability resultfunction symbolground termtree automatonunification problem

Mathematics Subject Classification ID

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

Recommendations

• Unification in sort theories and its applications
• scientific article; zbMATH DE number 4049132
• scientific article; zbMATH DE number 4049131
• A practically efficient and almost linear unification algorithm
• Decidable higher-order unification problems
• Decidability of bounded higher-order unification
• scientific article; zbMATH DE number 1948184
• scientific article; zbMATH DE number 1189058
• An ordering linear unification algorithm
• scientific article; zbMATH DE number 3866609

Cites work

• Computational aspects of an order-sorted logic with term declarations
• Equality and disequality constraints on direct subterms in tree automata
• scientific article; zbMATH DE number 1142316 (Why is no real title available?)
• scientific article; zbMATH DE number 834570 (Why is no real title available?)
• Inductive proofs by specification transformations
• Pumping, cleaning and symbolic constraints solving
• Unification in sort theories and its applications
• Unification theory

Cited in

(2)

• Unification in sort theories and its applications
• scientific article; zbMATH DE number 1189060 (Why is no real title available?)

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

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q4647533)