Extending finite model searching with congruence closure computation

DOI10.1007/978-3-540-30210-0_9MaRDI QIDQ5464721zbMATH OpenOpenAlexFDO

Authors Jian Zhang, Hantao Zhang

Publication date 19 August 2005

Published in Lecture Notes in Computer Science (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/b100361

Mathematics Subject Classification ID

Problem solving in the context of artificial intelligence (heuristics, search strategies, etc.) (68T20)

Recommendations

• Two techniques to improve finite model search
• The logic of constraint satisfaction
• Constraint propagation for first-order logic and inductive definitions
• Computing congruent closures on terms
• Constraint programming for modelling and solving modal satisfiability

Cited in

(4)

• Two techniques to improve finite model search
• Constraint solving for finite model finding in SMT solvers
• MACE4 and SEM: a comparison of finite model generators
• scientific article; zbMATH DE number 1389646 (Why is no real title available?)

Describes a project that uses

Uses Software

• FINDER

This page was built for publication: Extending finite model searching with congruence closure computation

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q5464721)