{"@context":"https:\/\/schema.org\/","@type":"PublicationVolume","@id":"#volume587","volumeNumber":5431,"name":"Dagstuhl Seminar Proceedings, Volume 5431","dateCreated":"2006-04-25","datePublished":"2006-04-25","isAccessibleForFree":true,"publisher":"Schloss Dagstuhl \u2013 Leibniz-Zentrum f\u00fcr Informatik","isPartOf":{"@type":"Periodical","@id":"#series119","name":"Dagstuhl Seminar Proceedings","issn":"1862-4405","isAccessibleForFree":true,"publisher":"Schloss Dagstuhl \u2013 Leibniz-Zentrum f\u00fcr Informatik","hasPart":"#volume587"},"hasPart":[{"@type":"ScholarlyArticle","@id":"#article1298","name":"05431 Abstracts Collection \u2013 Deduction and Applications","abstract":"From 23.10.05 to 28.10.05, the Dagstuhl Seminar 05431 ``Deduction and Applications'' was held\r\nin the International Conference and Research Center (IBFI),\r\nSchloss Dagstuhl.\r\nDuring the seminar, several participants presented their current\r\nresearch, and ongoing work and open problems were discussed. Abstracts of\r\nthe presentations given during the seminar as well as abstracts of\r\nseminar results and ideas are put together in this paper. The first section\r\ndescribes the seminar topics and goals in general.\r\nLinks to extended abstracts or full papers are provided, if available.","keywords":["Formal logic","deduction","artificial intelligence"],"author":[{"@type":"Person","name":"Baader, Franz","givenName":"Franz","familyName":"Baader"},{"@type":"Person","name":"Baumgartner, Peter","givenName":"Peter","familyName":"Baumgartner"},{"@type":"Person","name":"Nieuwenhuis, Robert","givenName":"Robert","familyName":"Nieuwenhuis"},{"@type":"Person","name":"Voronkov, Andrei","givenName":"Andrei","familyName":"Voronkov"}],"position":1,"pageStart":1,"pageEnd":23,"dateCreated":"2006-05-08","datePublished":"2006-05-08","isAccessibleForFree":true,"license":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/legalcode","copyrightHolder":[{"@type":"Person","name":"Baader, Franz","givenName":"Franz","familyName":"Baader"},{"@type":"Person","name":"Baumgartner, Peter","givenName":"Peter","familyName":"Baumgartner"},{"@type":"Person","name":"Nieuwenhuis, Robert","givenName":"Robert","familyName":"Nieuwenhuis"},{"@type":"Person","name":"Voronkov, Andrei","givenName":"Andrei","familyName":"Voronkov"}],"copyrightYear":"2006","accessMode":"textual","accessModeSufficient":"textual","creativeWorkStatus":"Published","inLanguage":"en-US","sameAs":"https:\/\/doi.org\/10.4230\/DagSemProc.05431.1","publisher":"Schloss Dagstuhl \u2013 Leibniz-Zentrum f\u00fcr Informatik","isPartOf":"#volume587"},{"@type":"ScholarlyArticle","@id":"#article1299","name":"05431 Executive Summary \u2013 Deduction and Applications","abstract":"Formal logic provides a mathematical foundation for many areas of\r\n computer science. Logical languages are used as specification\r\n language within, e.g., program development and verification,\r\n hardware design and verification, relational databases, and many\r\n subfields of Artificial Intelligence. Automated Deduction is\r\n concerned with the design and implementation of algorithms based on\r\n logical deduction for solving problems in these areas.\r\n\r\n The last years have seen considerable improvements concerning both\r\n basic automated deduction technology and its (real-world)\r\n applications. Accordingly, the goal of the seminar was to bring\r\n together researchers from both sides in order to get an overview of\r\n the state of the art, and also to get ideas how to advance automated\r\n deduction from an application oriented point of view.","keywords":["Formal logic","deduction","artificial intelligence"],"author":[{"@type":"Person","name":"Baader, Franz","givenName":"Franz","familyName":"Baader"},{"@type":"Person","name":"Baumgartner, Peter","givenName":"Peter","familyName":"Baumgartner"},{"@type":"Person","name":"Nieuwenhuis, Robert","givenName":"Robert","familyName":"Nieuwenhuis"},{"@type":"Person","name":"Voronkov, Andrei","givenName":"Andrei","familyName":"Voronkov"}],"position":2,"pageStart":1,"pageEnd":3,"dateCreated":"2006-04-25","datePublished":"2006-04-25","isAccessibleForFree":true,"license":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/legalcode","copyrightHolder":[{"@type":"Person","name":"Baader, Franz","givenName":"Franz","familyName":"Baader"},{"@type":"Person","name":"Baumgartner, Peter","givenName":"Peter","familyName":"Baumgartner"},{"@type":"Person","name":"Nieuwenhuis, Robert","givenName":"Robert","familyName":"Nieuwenhuis"},{"@type":"Person","name":"Voronkov, Andrei","givenName":"Andrei","familyName":"Voronkov"}],"copyrightYear":"2006","accessMode":"textual","accessModeSufficient":"textual","creativeWorkStatus":"Published","inLanguage":"en-US","sameAs":"https:\/\/doi.org\/10.4230\/DagSemProc.05431.2","publisher":"Schloss Dagstuhl \u2013 Leibniz-Zentrum f\u00fcr Informatik","isPartOf":"#volume587"},{"@type":"ScholarlyArticle","@id":"#article1300","name":"Automatically Generating Loop Invariants Using Quantifier Elimination","abstract":"An approach for automatically generating loop invariants using\r\nquantifier-elimination is proposed. An invariant of a loop is hypothesized as\r\na parameterized formula. Parameters in the invariant are discovered by generating\r\nconstraints on the parameters by ensuring that the formula is indeed\r\npreserved by the execution path corresponding to every basic cycle of the loop.\r\nThe parameterized formula can be successively refined by considering execution\r\npaths one by one; heuristics can be developed for determining the order in\r\nwhich the paths are considered. Initialization of program variables as well as\r\nthe precondition and postcondition of the loop, if available, can also be used\r\nto further refine the hypothesized invariant. Constraints on parameters generated\r\nin this way are solved for possible values of parameters. If no solution is\r\npossible, this means that an invariant of the hypothesized form does not exist\r\nfor the loop. Otherwise, if the parametric constraints are solvable, then under\r\ncertain conditions on methods for generating these constraints, the strongest\r\npossible invariant of the hypothesized form can be generated from most general\r\nsolutions of the parametric constraints. The approach is illustrated using the\r\nfirst-order theory of polynomial equations as well as Presburger arithmetic.","keywords":["Program verification","loop invariants","inductive assertions","quantifier elimination"],"author":{"@type":"Person","name":"Kapur, Deepak","givenName":"Deepak","familyName":"Kapur"},"position":3,"pageStart":1,"pageEnd":17,"dateCreated":"2006-04-25","datePublished":"2006-04-25","isAccessibleForFree":true,"license":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/legalcode","copyrightHolder":{"@type":"Person","name":"Kapur, Deepak","givenName":"Deepak","familyName":"Kapur"},"copyrightYear":"2006","accessMode":"textual","accessModeSufficient":"textual","creativeWorkStatus":"Published","inLanguage":"en-US","sameAs":"https:\/\/doi.org\/10.4230\/DagSemProc.05431.3","publisher":"Schloss Dagstuhl \u2013 Leibniz-Zentrum f\u00fcr Informatik","isPartOf":"#volume587"},{"@type":"ScholarlyArticle","@id":"#article1301","name":"On Algorithms and Complexity for Sets with Cardinality Constraints","abstract":"Complexity of data structures in modern programs presents a\r\nchallenge for current analysis and verification tools,\r\nforcing them to report false alarms or miss errors. I will\r\ndescribe a new approach for verifying programs with complex\r\ndata structures. This approach builds on program analysis\r\ntechniques, as well as decision procedures and theorem\r\nprovers.\r\n\r\nThe approach is based on specifying interfaces of data\r\nstructures by writing procedure preconditions and\r\npostconditions in terms of abstract sets and relations. Our\r\nsystem then separately verifies that 1) each data structure\r\nconforms to its interface, 2) each data structure interface\r\nis used correctly, and 3) desired high-level\r\napplication-specific invariants hold. The system verifies\r\nthese conditions by combining decision procedures, theorem\r\nprovers, and static analyses, promising an unprecedented\r\ntradeoff between precision and scalability. In the context\r\nof this system, we have developed new decision procedures\r\nfor reasoning about sets and their cardinalities, approaches\r\nfor extending the applicability of existing decision\r\nprocedures, and techniques for modular analysis of\r\ndynamically created data structure instances.","keywords":["Static analysis","data structure consistency","program verification","decision procedures"],"author":[{"@type":"Person","name":"Kuncak, Viktor","givenName":"Viktor","familyName":"Kuncak"},{"@type":"Person","name":"Rinard, Martin","givenName":"Martin","familyName":"Rinard"},{"@type":"Person","name":"Marnette, Bruno","givenName":"Bruno","familyName":"Marnette"}],"position":4,"pageStart":1,"pageEnd":0,"dateCreated":"2006-04-25","datePublished":"2006-04-25","isAccessibleForFree":true,"license":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/legalcode","copyrightHolder":[{"@type":"Person","name":"Kuncak, Viktor","givenName":"Viktor","familyName":"Kuncak"},{"@type":"Person","name":"Rinard, Martin","givenName":"Martin","familyName":"Rinard"},{"@type":"Person","name":"Marnette, Bruno","givenName":"Bruno","familyName":"Marnette"}],"copyrightYear":"2006","accessMode":"textual","accessModeSufficient":"textual","creativeWorkStatus":"Published","inLanguage":"en-US","sameAs":"https:\/\/doi.org\/10.4230\/DagSemProc.05431.4","publisher":"Schloss Dagstuhl \u2013 Leibniz-Zentrum f\u00fcr Informatik","isPartOf":"#volume587"},{"@type":"ScholarlyArticle","@id":"#article1302","name":"Proof Presentation","abstract":"The talk is based on a book about the human-oriented presentation of a mathematical proof in natural\r\nlanguage, in a style as we may find it in a typical mathematical text book.\r\nHow can a proof be other than human-oriented?\r\nWhat we have in mind is a deduction systems, which is implemented on a computer,\r\nthat proves \u2013 with some human interaction \u2013 a mathematical textbook as may be used\r\nin an undergraduate course. The proofs generated by these systems today are far from\r\nbeing human-oriented and can in general only be read by an expert in the respective\r\nfield: proofs between several hundred (for a common mathematical theorem), for more\r\nthan a thousand steps (for an unusually difficult theorem) and more than ten thousand\r\ndeduction steps (in a program verification task) are not uncommon.\r\nAlthough these proofs are provably correct, they are typically marred by many problems:\r\nto start with, that are usually written in a highly specialised logic such as the\r\nresolution calculus, in a matrix format, or even worse, they may be generated by a\r\nmodel checker. Moreover they record every logical step that may be necessary for the\r\nminute detail of some term transformation (such as, for example, the rearrangement of\r\nbrackets) along side those arguments, a mathematician would call important steps or\r\nheureka-steps that capture the main idea of the proof. Only these would he be willing\r\nto communicate to his fellow mathematicians \u2013 provided they have a similar academic\r\nbackground and work in the same mathematical discipline. If not, i.e. if the proof was\r\nwritten say for an undergraduate textbook, the option of an important step may be\r\nviewed differently depending on the intended reader.\r\nNow, even if we were able to isolate the ten important steps \u2013 out of those hundreds\r\nof machine generated proof steps \u2013 there would still be the startling problem\r\nthat they are usually written in the \"wrong\" order. A human reader might say: \"they do\r\nnot have a logical structure\"; which is to say that of course they follow a logical pattern\r\n(as they are correctly generated by a machine), but, given the convention of the respective\r\nfield and the way the trained mathematician in this field is used to communicate,\r\nthey are somewhat strange and ill structured.\r\nAnd finally, there is the problem that proofs are purely formal and recorded in a\r\npredicate logic that is very far from the usual presentation that relies on a mixture\r\nof natural language arguments interspersed with some formalism.\r\nThe book (about 800 page) which gives an answer to some of these problems is to appear with Elsevier","keywords":["Artificial intelligence","mathematics","proof presentation"],"author":{"@type":"Person","name":"Siekmann, J\u00f6rg","givenName":"J\u00f6rg","familyName":"Siekmann"},"position":5,"pageStart":1,"pageEnd":7,"dateCreated":"2006-05-08","datePublished":"2006-05-08","isAccessibleForFree":true,"license":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/legalcode","copyrightHolder":{"@type":"Person","name":"Siekmann, J\u00f6rg","givenName":"J\u00f6rg","familyName":"Siekmann"},"copyrightYear":"2006","accessMode":"textual","accessModeSufficient":"textual","creativeWorkStatus":"Published","inLanguage":"en-US","sameAs":"https:\/\/doi.org\/10.4230\/DagSemProc.05431.5","publisher":"Schloss Dagstuhl \u2013 Leibniz-Zentrum f\u00fcr Informatik","isPartOf":"#volume587"},{"@type":"ScholarlyArticle","@id":"#article1303","name":"Proving and Disproving Termination in the Dependency Pair Framework","abstract":"The dependency pair framework is a new general concept to integrate \r\narbitrary techniques for termination analysis of term rewriting. \r\nIn this way, the benefits of different techniques can be combined and \r\ntheir modularity and power are increased significantly. Moreover, this \r\nframework facilitates the development of new methods for termination analysis.\r\n\r\nTraditionally, the research on termination focused on methods which\r\nprove termination and there were hardly any approaches for disproving\r\ntermination. We show that with the dependency pair framework, one\r\ncan combine the search for a proof and for a disproof of termination. \r\nIn this way, we obtain the first powerful method which can also\r\nverify non-termination of term rewrite systems.\r\n\r\nWe implemented and evaluated our contributions in the automated termination\r\nprover AProVE. Due to these results, AProVE was the winning tool in the\r\nInternational Competition of Termination Provers 2005, both for proving and\r\nfor disproving termination of term rewriting.","keywords":["Termination","non-termination","term rewriting","dependency pairs"],"author":[{"@type":"Person","name":"Giesl, J\u00fcrgen","givenName":"J\u00fcrgen","familyName":"Giesl"},{"@type":"Person","name":"Thiemann, Ren\u00e9","givenName":"Ren\u00e9","familyName":"Thiemann"},{"@type":"Person","name":"Schneider-Kamp, Peter","givenName":"Peter","familyName":"Schneider-Kamp"}],"position":6,"pageStart":1,"pageEnd":1,"dateCreated":"2006-04-25","datePublished":"2006-04-25","isAccessibleForFree":true,"license":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/legalcode","copyrightHolder":[{"@type":"Person","name":"Giesl, J\u00fcrgen","givenName":"J\u00fcrgen","familyName":"Giesl"},{"@type":"Person","name":"Thiemann, Ren\u00e9","givenName":"Ren\u00e9","familyName":"Thiemann"},{"@type":"Person","name":"Schneider-Kamp, Peter","givenName":"Peter","familyName":"Schneider-Kamp"}],"copyrightYear":"2006","accessMode":"textual","accessModeSufficient":"textual","creativeWorkStatus":"Published","inLanguage":"en-US","sameAs":"https:\/\/doi.org\/10.4230\/DagSemProc.05431.6","publisher":"Schloss Dagstuhl \u2013 Leibniz-Zentrum f\u00fcr Informatik","isPartOf":"#volume587"}]}