Deciding \(\mathcal H_1\) by resolution

DOI10.1016/J.IPL.2005.04.007zbMath1185.68620OpenAlexW1552360561MaRDI QIDQ1041797

Jean Goubault-Larrecq

Publication date: 4 December 2009

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

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

zbMATH Keywords

formal languagesautomatic theorem proving

Mathematics Subject Classification ID

Formal languages and automata (68Q45)

Related Items (10)

Crossing the Syntactic Barrier: Hom-Disequalities for ${\mathcal H}_1$-Clauses ⋮ Tree automata with equality constraints modulo equational theories ⋮ Extending \(H_1\)-clauses with disequalities ⋮ Normalization of Linear Horn Clauses ⋮ The Blossom of Finite Semantic Trees ⋮ Rigid tree automata and applications ⋮ Paths, tree homomorphisms and disequalities for -clauses ⋮ Automated Verification of Equivalence Properties of Cryptographic Protocols ⋮ SPASS-AR: a first-order theorem prover based on approximation-refinement into the monadic shallow linear fragment ⋮ Automatic Verification of Security Protocols in the Symbolic Model: The Verifier ProVerif

Cites Work

• Haskell overloading is DEXPTIME-complete
• Abstraction and resolution modulo AC: How to verify Diffie--Hellman-like protocols automatically
• Paths vs. trees in set-based program analysis
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item

This page was built for publication: Deciding \(\mathcal H_1\) by resolution