Descente Infinie and Frameworks for Variables

Distinguished Visitor – Case for Support, Oct. 30, 2009

Murdoch J. Gabbay  Claus-Peter Wirth

The visiting researcher Claus-Peter Wirth has been a member of the Association for Automated Reasoning since 1994 and has worked in automated and human-oriented inductive theorem proving since 1990. He holds a Dr. rer. nat. from the University of Kaiserslautern in informatics, and was a member of the Collaborative Research Center SFB 378 “Resource-Adaptive Cognitive Processes” at the Saarland University for many years. After working at the Max Planck Institute for Informatics his current affiliation is the German Research Center for Artificial Intelligence.

His research work centres around the tacticbased human-oriented inductive theorem proving system QuodLibet [Avenhaus &al., 2003], which realizes Fermat’s descente infinie instead of the more restrictive explicit induction. For convenient recursive specification of partial functions, he developed a novel framework of positive/negative-conditional term rewriting [Wirth & Gramlich, 1994].

Amongst other confluence criteria [Gramlich & Wirth, 1996], [Dershowitz &al., 2009], he has developed the only criteria sufficient for (shallow) confluence of nonterminating, non-orthogonal conditional rewrite systems [Wirth, 2009]. His major contribution is a method to combine state-of-the-art freevariable deduction in any two-valued logic with Fermat’s descente infinie [Wirth, 2004]. The main tool in this method of combination is a new form of Hilbert’s ε, providing an operator of indefinite, but possibly committed choice [Wirth, 2002; 2006; 2008].

Project The visiting researcher will visit Edinburgh for six weeks in November-December 2009 or as soon as possible thereafter. He will work with Murdoch J. Gabbay (Heriot Watt University), with Alan Bundy and Alan Smaill (University of Edinburgh), and he will give talks on his research; if possible at SPLS and STP, and at departmental seminars throughout Scotland with interests in formal methods (including Heriot-Watt, Edinburgh, St Andrews, and Glasgow).

This project is relevant to the Complex Systems and the Modelling and Abstraction themes, and the leaders of the themes have given their support to this proposal.

Work at Heriot Watt University Both Gabbay and Wirth research the nature of variables. Gabbay’s research is motivated by the nominal techniques. These are a firstorder abstract theory of name-binding [Gabbay & Pitts, 2002] which include, amongst other things, in-built notions of dependence and independence between variables, with a rigorous semantics in nominal sets.

Wirth’s research is motivated by proofsearch, which must account for different kinds of variables (‘universal’ and ‘existential’ variables, and ‘committed choice’ variables related to Hilbert’s ϵ). Complex patterns of dependency between these different kinds of variable render this non-trivial. Wirth’s research attempts to manage this complexity and turn it to algorithmic advantage in a rigorous but simple system, but furthermore, he has a consistent interest in semantics for the constructs which then arise. Gabbay and Wirth have been in communication since 2003, discussing frameworks for the semantics of variables by Gabbay [2009], [Gabbay & Mathijssen, 2007; 2008], [Gabbay & Pitts, 2002], [Gabbay & Cheney, 2004], and their connection with the framework for the semantics of free variables by Wirth [2004; 2008], and on their respective calculi.

One third of the stay will be devoted to making common cause in researching these issues, and specifically laying out a grant proposal for joint research.

Work at University of Edinburgh Alan Bundy, Alan Smaill, and Wirth had submitted a proposal of a one-year project to EP-SRC on Fermat’s descente infinie (the standard mathematical form of induction) in program synthesis with excellent evaluation that was only third to the set of accepted proposals in January 2008. Due to Bundy, Edinburgh has become the Mecca for explicit induction and its avantgarde features in automated induction (such as rippling, higher-order logic, program synthesis) for decades now.

We cannot list the hundreds of relevant publications; a good survey is Bundy [1999].

Wirth developed the major competing paradigm to explicit induction and the chief designer of the descente infinie automated humanoriented inductive theorem prover QuodLibet [Avenhaus &al., 2003], [Kühler, 2000], [Schmidt-Samoa, 2006a; 2006b; 2006c].

One third of the stay will be devoted to resubmitting this proposal in revised form.

Talks The visiting researcher will give several research seminars. In particular, he will speak on the combination of analytical and synthetical reasoning with proof forests and on freevariable frameworks [Wirth, 2004], on Hilbert’s ε as a operator of indefinite choice [Wirth, 2008], on partial and non-terminating recursive specifications in induction and coinduction [Wirth, 2009], and perhaps too on his work on the Hilbert–Bernays Project [Gabbay &al., 2010ff.] (to publish a commented bilingual edition of the Hilbert Bernays Grundlagen der Mathematik).

Costs We estimate 300GBP for a return trip from Saarbrücken to Edinburgh and subsistence costs of 3400GBP for six weeks (700GBP for two weeks plus 500GBP for four weeks). Costs for travel within Scotland to give talks will be covered by subsistence, or by the host institution from their ‘visiting speaker’ budget. Heriot-Watt has agreed to waive bench fees, with a value of 500GBP. Edinburgh University has also kindly contributed 500GBP. We therefore request 3200GBP in total.

This project is excellent value for money and a good opportunity to lead to research collaborations and project proposals which will be of long-term benefit to Scottish research. Wirth’s talks will also be of general interest to postdoctoral and doctoral researchers.

References

[Anon, 2004] Anon, editor. 19th IEEE Symposium on Logic in Computer Science (LICS 2004), Turku, Finland. IEEE Computer Society, 2004.

[Avenhaus &al., 2003] Jürgen Avenhaus, Ulrich Kühler, Tobias Schmidt-Samoa, and Claus-Peter Wirth. How to prove inductive theorems? QuodLibet! In 19th Int. Conf. on Automated Deduction, Miami Beach (FL), 2003, number 2741 in Lecture Notes in Artificial Intelligence, pages 328–333. Springer, 2003.

http://www.ags.uni-sb.de/~cp/p/quodlibet.

[Bundy, 1999] Alan Bundy. The Automation of Proof by Mathematical Induction. Informatics Research Report No. 2, Division of Informatics, Univ. Edinburgh, 1999. Also in [Robinson & Voronkow, 2001, Vol. 1, pp. 845–911].

[Dershowitz &al., 2009] Nachum Dershowitz, Bernhard Gramlich, Mitsuhiro Okada, G. Sivakumar, and Claus-Peter Wirth. Conditional confluence. In preparation, 2009.

[Gabbay & Cheney, 2004] Murdoch J. Gabbay and James Cheney. A sequent calculus for nominal logic. 2004. In [Anon, 2004, pp. 139– 148].

[Gabbay & Mathijssen, 2007] Murdoch J. Gabbay and Aad Mathijssen. A formal calculus for informal equality with binding. 2007. In [Leivant & Queiroz, 2007, pp. 162–176].

[Gabbay & Mathijssen, 2008] Murdoch J. Gabbay and Aad Mathijssen. Capture-avoiding substitution as a nominal algebra. Formal Asp. Comput., 20:451–479, 2008. http://dx.doi.org/10.1007/

s00165-007-0056-1.

[Gabbay & Pitts, 2002] Murdoch J. Gabbay and Andrew M. Pitts. A new approach to abstract syntax with variable binding. Formal Asp. Comput., 13:341–363, 2002.

[Gabbay &al., 2010ff.] Dov Gabbay, Jörg Siekmann, and Claus-Peter

Wirth. Hilbert Bernays Project. http://www.ags.uni-sb.de/~cp/p/
hilbertbernays/goal.htm, 2010ff..

[Gabbay, 2009] Murdoch J. Gabbay. A study of substitution, using nominal techniques and Fraenkel–Mostowski sets. Theoretical Computer Sci., 410:1159–1189, 2009. http://dx.doi.org/10.1016/

j.tcs.2008.11.013.

[Gramlich & Wirth, 1996] Bernhard Gramlich and Claus-Peter Wirth. Confluence of terminating conditional term rewriting systems revisited. In 7th Int. Conf. on Rewriting Techniques and Applications, New Bruns wick (NJ), 1996, number 1103 in Lecture Notes in Computer Science, pages 245–259. Springer, 1996.

[Kühler, 2000] Ulrich Kühler. A Tactic-Based Inductive Theorem Prover for Data Types with Partial Operations. Infix, Akademische Verlagsgesellschaft Aka GmbH, Sankt Augustin, Berlin, 2000.

PhD thesis, http://www.ags.uni-sb.de/~cp/p/kuehlerdiss.

[Leivant & Queiroz, 2007] Daniel Leivant and Ruy J. G. B. de Queiroz, editors. Logic, Language, Information and Computation, 14th International Workshop, WoLLIC 2007, Rio de Janeiro, number 4576 in Lecture Notes in Computer Science. Springer, 2007.

[Robinson & Voronkow, 2001] Alan Robinson and Andrei Voronkow, editors. Handbook of Automated Reasoning. Elsevier, 2001.

[Schmidt-Samoa, 2006a]  Tobias Schmidt-Samoa.  An even closer

integration of linear arithmetic into inductive theorem proving. Electronic Notes in Theoretical Computer Sci., 151:3–

20, 2006. http://www.ags.uni-sb.de/~cp/p/evencloser, http://dx.doi.org/
10.1016/j.entcs.2005.11.020.

[Schmidt-Samoa, 2006b] Tobias Schmidt-Samoa. Flexible Heuristic Control for Combining Automation and User-Interaction in Inductive Theorem Proving. PhD thesis, Univ. Kaiserslautern, 2006.

http://www.ags.uni-sb.de/~cp/p/samoadiss.

[Schmidt-Samoa, 2006c] Tobias Schmidt-Samoa. Flexible heuristics for simplification with conditional lemmas by marking formulas as forbidden, mandatory, obligatory, and generous. Journal of Applied Non-Classical Logics, 16:209–239, 2006. http://dx.doi.org/

10.3166/jancl.16.208-239.

[Wirth & Gramlich, 1994] Claus-Peter Wirth and Bernhard Gramlich. A constructor-based approach for positive/negativeconditional equational specifications. J. Symbolic Computation,

17:51–90, 1994. http://www.ags.uni-sb.de/~cp/p/jsc94.

[Wirth, 2002] Claus-Peter Wirth. A new indefinite semantics for Hilbert’s epsilon. In Uwe Egly and Christian G. Fermüller, editors, 11th Int. Conf. on Tableaus and Related Methods, København, 2002, number 2381 in Lecture Notes in Artificial Intelligence,

pages 298–314. Springer, 2002. http://www.ags.uni-sb.de/~cp/p/epsi.

[Wirth, 2004] Claus-Peter Wirth. Descente Infinie + Deduction.

Logic J. of the IGPL, 12:1–96, 2004. http://www.ags.uni-sb.de/~cp/p/d.

[Wirth, 2006] Claus-Peter Wirth. Hilbert’s epsilon as an Operator of Indefinite Committed Choice. SEKI-Report SR–2006–02 (ISSN 1437–4447). SEKI Publications, Saarland Univ., 2006. http://arxiv.

org/abs/0902.3749, http://www.ags.uni-sb.de/~cp/p/epsi.

[Wirth, 2008] Claus-Peter Wirth. Hilbert’s epsilon as an operator of indefinite committed choice. J. Applied Logic, 6:287–317, 2008.

http://dx.doi.org/10.1016/j.jal.2007.07.009, http://www.ags.uni-sb.de/~cp/
p/epsi.

[Wirth, 2009] Claus-Peter Wirth. Shallow confluence of conditional term rewriting systems. J. Symbolic Computation, 44:69–98, 2009.

http://dx.doi.org/10.1016/j.jsc.2008.05.005.