In this column, I offer a strategy that may be new to most or all AAR members. The strategy, called the subformula strategy, has the objective of directing a program's reasoning in an effective manner. I offer two theorems to prove, each of which yielded rather quickly when the subformula strategy was used. In that logic is emphasized in a conference soon to be held, this column may prove of especial interest. The area of logic of concern is classical propositional calculus. This area admits many axiom systems, perhaps the most often cited being the following.
% Lukasiewicz 1 2 3. P(i(i(x,y),i(i(y,z),i(x,z)))). P(i(i(n(x),x),x)). P(i(x,i(n(x),y))).
The function symbol i denotes implication; the
function symbol n denotes negation; the predicate symbol
P denotes provability. The two theorems of interest focus,
respectively, on single axioms for this area of logic.
% Following is Meredith's 21-letter single axiom. P(i(i(i(i(i(x,y),i(n(z),n(u))),z),v),i(i(v,x),i(u,x)))). % Following is Lukasiewicz's 23-letter single axiom. P(i(i(i(x,y),i(i(i(n(z),n(u)),v),z)),i(w,i(i(z,x),i(u,x))))).
You are asked to derive the given three-axiom system from each of the two given single axioms, that of Meredith and that of Lukasiexicz. Before experimenting with the subformula strategy, you might enjoy seeking the two proofs with whatever approach you prefer. Then, I invite you to try the subformula strategy, which I explain in the following paragraph.
Subformula strategy. In this strategy, you take the target and/or the hypothesis and select all of its subformulas, excluding variables, but including the entire formula.
With William McCune's OTTER, you assign to each subformula a small weight, say, 1, which has the program treat the enclosed expression as having length 1. The basic idea is to enable the reasoning program in use to treat expressions as if they are shorter than if measured in symbol count.
The website automatedreasoning.net provides far more information about the subformula strategy and its use in the study of various areas of logic. The notebooks there offer challenges, open questions, input files (for OTTER), and much commentary. Although the notation is oriented to OTTER, the material is useful for other programs also.
The terms of Reiner Hähnle and Cesare Tinelli are expiring. The position of Alessandro Armando is taken by Renate Schmidt as CADE-22 program chair. Thus, there are two positions to fill.
The following candidates (listed in alphabetical order) were nominated and their statements are below:
Alessandro Armando
nominated by Maria Paola Bonacina and Amy Felty
Christoph Benzmüller
nominated by Serge Autexier and Larry Paulson
Reiner Hähnle
nominated by Franz Baader and Ulrich Furbach
Konstantin Korovin
nominated by Andrei Voronkov and Geoff Sutcliffe
Brigitte Pientka
nominated by Aaron Stump and Renate Schmidt
Cesare Tinelli
nominated by Reiner Hähnle and Wolfgang Ahrendt
Automated Deduction is not only one of the most exciting research topic of Artificial Intelligence, it is also the research area which is going to affect the way complex artifacts (e.g. hardware components, software systems, the future Internet) will be designed and built. Success will largely depend on our ability to undertake the foundational research issues underpinning the many practical problems posed by these application domains. To this end it crucially important that our community remains open to stimuli coming from other, more applied, research areas (such as Automated Verification, Semantic Web) as well as from research areas that explore complementary Automated Reasoning techniques (SAT, SMT, CP to name a few). CADE involvement in the IJCAR and FLoC initiatives are important steps in this direction which I wholeheartedly support.
My research in the past decade (mainly but not only at Saarland University, Germany) has been driven by a wide range of interests and activities related to automated and interactive theorem proving, proof planning, agent-based architectures in theorem proving, and natural language user interfaces to theorem provers. However, the main focus of my research has always been on the theory and automation of simple type theory. In a project at Cambridge I have recently developed the higher-order automated theorem LEO-II which cooperates with first order automated theorem provers. An important next move for improving the state of the art in automated higher-order theorem proving is to set up a higher-order TPTP infrastructure and to initiate a higher-order CASC at CADE -- this is part of the ongoing collaboration with Geoff Sutcliffe (and others) in EU project THFTPTP.
I have been very active at CADE and IJCAR conferences in the past (8 papers at CADE and IJCAR, organizer of several workshops) and I am a strong supporter of IJCAR and FLOC. It is important that the CADE community continues its recent policy to accept more implementation and application oriented papers while at the same time maintaining very high research quality standards. I highly welcome more interaction with users and potential users of automated theorem provers at CADE and IJCAR -- a good example has been the third party sponsored, new CASC problem class division(s) on large theories --- with the aim to foster applicability and visibility of our tools in practice and to gain new research stimuli.
The first international scientific conference that I attended was CADE-8 in 1986. Ever since, the CADE community has been one of the major venues where my professional career took place. I served on most CADE (and IJCAR) PCs in the last 10 years, was conference chair of CADE-18 in Copenhagen, and I will be IJCAR PC co-chair in 2010.
Having worked on automated reasoning in non-classical and first-order logics in the past, my current research interests lie mainly within software verification. To ensure the continued existence of automated deduction as a dynamic and lively field of research I believe it is important that CADE increases the participation of consumers of reasoning technology such as formal verification, test case generation, semantic web, etc.
In the past years I served on the steering committees of CADE, FLoC, IJCAR, Tableaux, and FTP. I was involved in the foundation of both IJCAR and Tableaux. From this experience I gained considerable insight into the structure and current status of various subcommunities of computational logic. I believe that the field needs both, highly visible, comprehensive meetings (such as IJCAR and FLoC) as well as more intimate and specialized ones, which subcommunities can identify with.
If elected to a second term as CADE trustee I will concentrate on the following issues:
My research work focuses on both theoretical and implementation aspects of first-order reasoning. I have been working on ordering constraint solving, orientability problems, AC-orderings and more recently, on instantiation based methods and integration of theory reasoning into first-order logic. I have been developing and implementing iProver -- an instantiation-based theorem prover for first-order logic.
CADE is the leading conference in automated reasoning and we have seen a number of success stories at CADE including: first-order theorem proving and term rewriting, interactive theorem proving and higher order logics, satisfiability modulo theories and computer algebra, reasoning with ontologies and description logics, automata techniques and modal logics. CADE has excelled in combining diverse areas and I believe that CADE could further promote rapidly growing and exciting areas. I strongly support the organisation of workshops co-located with CADE, as this helps to attract research work from bordering areas, which are usually published in other conferences such as CAV, RTA, LICS, ICALP, TPHOL and IJCAI.
Another attractive aspect of CADE is that it keeps a good balance between theoretical work, implementation and applications. I believe that CADE can further strengthen interaction between the research community and real-world applications. Industrial partners can be further encouraged to contribute to CADE. I strongly support the development of new systems and the organisation of competitions such as CASC, which help to demonstrate possibilities of the state-of-the-art systems to industrial users and conversely, propagate problems from real-world applications to the research community.
To conclude, as a CADE trustee, I would be very keen in supporting and promoting high quality theoretical research, exciting new research directions, development of reasoning systems and applications of automated reasoning.
In my view, CADE is the major venue for all aspects of automated reasoning research, and I regard it as the driving force to promote our field. While we should continue our emphasis on theoretical work and system building, I believe we should also reach out and welcome applications of our work in areas such as computer algebra, constraint solving, knowledge representation, mechanization of programming languages, and reasoning about programs. To foster synergy with other related areas, I would like to initiate discussions about collocating CADE with conferences on related areas. Joint events such as IJCAR and collocating with FLOC are also important ways to promote the visibility of our area and demonstrate the impact of our results to the general computer science community at large. My own research interest is in the theory and practice of logical frameworks. This includes: designing and investigating type theories and logics, building efficient verification and programming tools, and demonstrating their effectiveness using realistic applications. Since 2001, I have regularly published at CADE/IJCAR, ICLP, and, most recently, TPHOLs, POPL and PPDP. In 2003, I received the best paper award at ICLP'03 for my work on higher-order term indexing, and I was invited to give a tutorial at ICLP'06 about my work. Over the past few years, I have been actively involved in promoting our field, and I will be hosting CADE in Montreal in 2009. Over the previous years I was publicity chair for CADE 2005, PC member (PPDP'04, MFPS'05, ICLP'06, LPAR'07, ICLP'08, ICFP'08, CADE'09), organizer (2006, 2007) and program chair (2006) of the "Workshop for Logical Frameworks and Meta-theory: Theory and Practice," and area editor (theorem proving) for the Association of Logic Programming Newsletter (since 2005). As a CADE trustee, I intend to continue working toward ensuring that automated reasoning receives the attention it deserves.
My general research interests are automated reasoning, with a focus on satisfiability modulo theories. I have been particularly active in the combination of decision procedures and their integration into general purpose calculi, and in the application of SMT techniques in verification. I'm the co-founder of the SMT workshop (formerly PDPAR), now getting ready for its 7th edition. I have served as a PC member or co-organizer for a number of AR related events (see my web page for a complete list), as well as in the steering committees of FTP, FroCoS and IJCAR. I'm also a coordinator of the SMT-LIB initiative, whose main goal is to establish common standards and a library of benchmarks for satisfiability modulo theories. In that capacity, I maintain active contacts with a large number of computer-aided verification practitioners and researchers from industry and academia, who have many potential applications for and a strong interest in SMT.
As a trustee I would push for CADE to continue its efforts in attracting papers over the whole spectrum of AR research, with a continued emphasis on attracting more work on applications. I would use my ties to a now well-established community of SMT researchers (many of which do not come from the AR community) to help maintain a continued flow of CADE submissions from them. I would also work toward making the CADE community more aware of the sort of deduction problems faced in verification, and the pressing need in that field for a variety of automated deduction tools and technologies.
Registration is now in full swing for LPAR 2008, which will take place November 23-27, 2008 in Doha, Qatar.
Workshops held together with LPAR 2008 are:
The early registration deadline is 3 November 2008. See the conference web pages for details.
The International Conference on Verification, Model Checking, and Abstract Interpretation will take place January 18–20, 2009 in Savannah, Georgia, USA, co-located with POPL 2009.
The broad range of topics includes deductive methods and program verification, which might be interesting for some of the AAR community! See the list of accepted papers at the Conference web site.
WoLLIC 2009 will take place at the National Institute of Informatics in Tokyo, Japan, June 21-24, 2009.
WoLLIC is an annual international forum on inter-disciplinary research involving formal logic, computing and programming theory, and natural language and reasoning. Accordingly papers on papers on cross-disciplinary subjects are of particular interest.
Although the event is nominally a workshop, proceedings are to be published in Springer's LNCS series.
The deadline for submissions is 8 March 2009. For further details, see the event's web pages.
RDP'09 will take place 28. June–3. July 2009 in Brasilia, Brazil.
RDP'09 is a federated event comprising two major conferences:
In addition, the School on Rewriting, Type Theory, and Applications will take place the week before RDP.
RDP solicits proposals for satellite workshops of RDP'09 that are related in topics to one or both of the RDP conferences. Please see the call for proposals web page for more details.
Deadline for workshop proposals: 17 November 2008
RTA submission deadline: 26 January 2009
TLCA submission deadline: 12 January 2009 For further details, see the RDP web pages.
The next International Conference on Automated Reasoning with Analytic Tableaux and Related Methods will take place in Oslo, Norway, 6.–10. July 2009. Topics of interest include (but are not restricted to):
Papers about applications are particularly encouraged!
Workshop & tutorial proposal submission: Friday, 9 January 2009
Research paper submission: Monday, 26 January 2009
For full details about this event, please refer to the conference web pages
Next year's International Conference on Automated Deductions will be hosted by McGill University, Montreal, Canada August 2–7, 2009.
CADE is the major forum for the presentation of research in all aspects of automated deduction.
The submission deadline is 23 February 2009. See here for full details on this conference.
There is also a call for Workshop and Tutorial proposals with submission deadline December 7, 2008. Again, see the CADE web pages for details!
Next year's IEEE Symposium on Logic in Computer Science will be held at UCLA, Los Angeles, California, USA, 11th–14th August 2009. It will be colocated with the 16th International Static Analysis Symposium (SAS 2009), 9th–11th August 2009.
Topics of interest include any theoretical and practical topics in computer science that relate to logic broadly construed, but automated deduction is among the topics explicitly listed in the call for papers.
The paper submission deadline is 19 January 2009. Refer to the conference web pages for details.
ICTAC 2009, the 6th International Colloquium on Theoretical Aspects of Computing will be held on 18–20 August 2009 at Kuala Lumpur, Malaysia.
Topics of interest include theorem proving, software verification, logics and their applications, and many more.
The submission deadline is 1 April 2009. See here for details.
The next International Symposium on Formal Methods, FM 2009, will take place at Eindhoven, the Netherlands, 30 October–7 November 2009.
The conference calls for "papers on every aspect of the development and application of formal methods for the improvement of the current practice on system developments.", so some applications of automated reasoning are definitely in scope.
The paper submission deadline is 4 May, 2009. Refer to the conference web pages for details.
The WING 2009 Workshop on Invariant Generation will be held as a satellite workshop of ETAPS 2009 on 22–23 March 2009, at the University of York, UK.
Generally, WING welcomes submissions presenting novel methods to support reasoning about loops in programs, including methods based on automated reasoning.
The paper submission deadline is 12 January, 2009. See the event web page for further details.
The Annals of Mathematics and Artificial Intelligence (AMAI) will publish a special issue on the topic of application of Constraints to Formal Verification and AI (CFVAI), edited by Miroslav Velev and John Franco.
Topics include, but are not limited to, the following:
Submissions have to be in the AMAI format and have to be e-mailed to: mvelev (at) gmail.com until November 30, 2008.
AI Communications will publish a special issue on Practical Aspects of Automated Reasoning, following the PAAR workshop at IJCAR earlier this year.
Topics of interest include:
The paper submission deadline is 22 December 2008. See the full Call for Papers for details.
The Department of Computer Science of the Università degli Studi di Verona, in beautiful Verona, Italy, has one opening for a post-doc position in
Automated Reasoning applied to Program Analysis
The position is for one year (12 months) renewable for a second year. The position is funded in part by the University and in part by a research grant entitled "Design and integration of proof engines for program analysis". However, the successful applicant is welcome to contribute topics: the position is full-time on research (no teaching assignments) so that there is time and freedom to pursue more than one direction. Recent Ph.D. graduates or Ph.D. students very close to graduation in Computer Science or related field with a thesis in automated reasoning (broadly meant) are kindly invited to write by e-mail, attaching their Curriculum Vitae with a research statement, to:
Prof. Maria Paola Bonacinafor further details and discussion of research interests. The position should be filled by April 2009. Applications will be considered as soon as received.
For those of us into semantic technology and ontology engineering, a submission to the SUMO prize might be worth considering!
The SUMO prize is for the best open source ontology extension of SUMO, the Suggested Upper Merged Ontology, which, according to the web site, together with "its domain ontologies form the largest formal public ontology in existence today".
The SUMO prize for US$3000.00 is awarded each year to the best open source project that extends SUMO. Entries are due electronically to Adam Pease (apease [at] articulatesoftware [dot] com) by December 1. Awards will be made December 31 each year. Entries must be SUO-KIF files that extend SUMO and its domain ontologies, and conform to them.
In addition to the logical soundness of the ontology with respect to the SUMO ontologies, entries will be judged on several criteria:
For more detail see here.
Second-Order Quantifier Elimination
Foundations, Computational Aspects and Applications
by
Dov M. Gabbay, Renate A. Schmidt, and Andrzej Szalas
Studies in Logic: Mathematical Logic and Foundations, Vol. 12
College Publications 2008, 308 pages
ISBN 978-1-904987-56-7
In recent years there has been an increasing use of logical methods and significant new developments have been spawned in several areas of computer science, ranging from artificial intelligence and software engineering to agent-based systems and the semantic web. In the investigation and application of logical methods there is a tension between:
Second-order logics are very expressive and allow us to represent domain knowledge with ease, but there is a high price to pay for the expressiveness. Most second-order logics are incomplete and highly undecidable. It is the quantifiers which bind relation symbols that make second-order logics computationally unfriendly. It is therefore desirable to eliminate these second-order quantifiers, when this is mathematically possible; and often it is. If second-order quantifiers are eliminable we want to know under which conditions, we want to understand the principles and we want to develop methods for second-order quantifier elimination. This book provides the first comprehensive, systematic and uniform account of the state-of-the-art of second-order quantifier elimination in classical and non-classical logics. It covers the foundations, it discusses in detail existing second-order quantifier elimination methods, and it presents numerous examples of applications and non-standard uses in different areas. These include:
The book is intended for anyone interested in the theory and application of logics in computer science and artificial intelligence.
Further information can be found at The book's web page