Tree automata with equality constraints modulo equational theories

DOI10.1016/j.jlap.2007.10.006zbMath1137.68035OpenAlexW1967865708MaRDI QIDQ2426520

Florent Jacquemard, Michaël Rusinowitch, Laurent Vigneron

Publication date: 22 April 2008

Published in: The Journal of Logic and Algebraic Programming (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1016/j.jlap.2007.10.006

zbMATH Keywords

splittingtree automatabasic paramodulationfirst-order theorem provingverification of infinite state systems

Mathematics Subject Classification ID

Formal languages and automata (68Q45) 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)

Related Items

Tree automata with equality constraints modulo equational theories, Automated Induction with Constrained Tree Automata, TREE AUTOMATA WITH GLOBAL CONSTRAINTS, Rigid tree automata and applications, Rigid Tree Automata

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Deciding \(\mathcal H_1\) by resolution
• Haskell overloading is DEXPTIME-complete
• Basic paramodulation
• Automata for reduction properties solving
• Tree automata with equality constraints modulo equational theories
• Pumping, cleaning and symbolic constraints solving
• Equality and disequality constraints on direct subterms in tree automata
• Mobile values, new names, and secure communication
• STACS 2004
• CONCUR 2005 – Concurrency Theory