Search for Finite Models of First-order Theories: Techniques and Applications

Dr Jian Zhang

Laboratory of Computer Science
Institute of Software, Chinese Academy of Sciences

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.

ASTEC seminar
May 30, 2000

Place: Information technology, Uppsala University
Room: 1549
Time: 15.30 (+ coffee and discussion)

Room 1549 is in Building 1, Floor 5, room 49
(in the northern part of the building).

Help on how get here and MIC campus drawing.

There will be an extended period for discussions after the seminar nourished by cookies and coffee.

Speakers are encouraged to give an short (5 min) introduction to the subject at the begining of the talk.
Listeners are excused if they have to leave after 1 hour.

Updated 29-May-2000 14:40 by Roland Grönroos
e-mail: info -at-    Location: