Search for Finite Models of First-order Theories: Techniques and Applications
Dr Jian Zhang
Laboratory of Computer Science
The satisfiability problem in the first-order logic is undecidable in general. For the past 10 years, various researchers have studied the automatic generation of finite models of first-order theories. Given a set of axioms and a fixed positive integer n, the existence of models of size n can be determined by exhaustive search. But the time complexity is high. In this talk, I will describe techniques for reducing the search space, existing tools for model searching and applications such as the analysis of formal specifications. A concurrent decision procedure for propositional modal logics will also be presented.