Tree automata with equality constraints modulo equational theories

DOI10.1016/j.jlap.2007.10.006zbMath1137.68035MaRDI 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

splitting; tree automata; basic paramodulation; first-order theorem proving; verification of infinite state systems

Mathematics Subject Classification ID

68Q45: Formal languages and automata

03D05: Automata and formal grammars in connection with logical questions

03B25: Decidability of theories and sets of sentences

03B35: Mechanization of proofs and logical operations

Related Items

Rigid tree automata and applications, Tree automata with equality constraints modulo equational theories, Automated Induction with Constrained Tree Automata, TREE AUTOMATA WITH GLOBAL CONSTRAINTS, 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