Extending \(H_1\)-clauses with disequalities

DOI10.1016/J.IPL.2011.07.011zbMath1260.68115OpenAlexW2000550348MaRDI QIDQ1944188

Andreas Reuß, Helmut Seidl

Publication date: 4 April 2013

Published in: Information Processing Letters (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1016/j.ipl.2011.07.011

zbMATH Keywords

Horn clausesformal methodsprogram analysisfinite tree automata\(H_{1}\)-normalizationterm disequalities

Mathematics Subject Classification ID

Formal languages and automata (68Q45) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30)

Related Items (3)

Crossing the Syntactic Barrier: Hom-Disequalities for ${\mathcal H}_1$-Clauses ⋮ Paths, tree homomorphisms and disequalities for -clauses ⋮ SPASS-AR: a first-order theorem prover based on approximation-refinement into the monadic shallow linear fragment

Cites Work

• Unnamed Item
• Unnamed Item
• Deciding \(\mathcal H_1\) by resolution
• Bottom-Up Tree Automata with Term Constraints
• Verification, Model Checking, and Abstract Interpretation
• Verification, Model Checking, and Abstract Interpretation

This page was built for publication: Extending \(H_1\)-clauses with disequalities