Unification in pseudo-linear sort theories is decidable

DOI10.1007/3-540-61511-3_99zbMATH Open1415.03033OpenAlexW1562994860MaRDI QIDQ4647533FDOQ4647533

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

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

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

• Title not available (Why is that?)
• Equality and disequality constraints on direct subterms in tree automata
• Title not available (Why is that?)
• 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

Cited In (1)

• Title not available (Why is that?)

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)