Extending \(H_1\)-clauses with disequalities
From MaRDI portal
Publication:1944188
DOI10.1016/j.ipl.2011.07.011zbMath1260.68115MaRDI QIDQ1944188
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
Horn clauses; formal methods; program analysis; finite tree automata; \(H_{1}\)-normalization; term disequalities
68Q45: Formal languages and automata
68N30: Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.)
Related Items
Paths, tree homomorphisms and disequalities for -clauses, SPASS-AR: a first-order theorem prover based on approximation-refinement into the monadic shallow linear fragment, Crossing the Syntactic Barrier: Hom-Disequalities for ${\mathcal H}_1$-Clauses
Cites Work