 |
LIMBS Seminars |
|
LIMBS Seminars |
June
4th 2pm "auletta di rappresentanza 1 piano"
Speaker: Predrag JANICIC, University of Beograd (Serbia)
Title: Automatic Synthesis of Decision Procedures: a Case Study of Ground and Linear Arithmetic
Abstract:
In this talk the problem of automatic synthesis of decision procedures will
be discussed. Our approach (this is joint work with Alan Bundy) is evaluated on
ground arithmetic and Fourier/Motzkin decision procedure for linear arithmetic,
but the it can be applied to other domains as well. The approach is well-suited
to the proof-planning paradigm. The synthesis mechanism consists of several
stages and submechanisms. Some of these steps are performed automatically, while
in some steps human interaction is necessary.
Our system synthesized a decision procedure for ground arithmetic completely automatically and it used some specific method generators in generating a decision procedure for linear arithmetic. We believe that this approach can lead to automated assistance in constructing decision procedures and to more reliable implementations of decision procedures.
CV
Dr. JANICIC is assistant professor at the Faculty of Mathematics, University of Beograd, Serbia. Besides other activities, he has recently been working in computer Science at the School of Informatics, University of Edinburgh, with Prof. Alan Bundy. His current research focusses on automatic synthesis of decision procedures (http://www.matf.bg.ac.yu/~janicic)