| Abstract: | The quest for proved and reliable software goes through theorem provers, which implement proof search. A main trend of these last ten years has been the combination of assisted and automated deduction. Different approaches to this integration are currently studied focussing on efficiency and/or reliability. A promising research direction is to provide formal systems, programming languages and proof environments that support and integrate the two paradigms of computation and deduction. This revised version was published online in June 2006 with corrections to the Cover Date. |
