Algebra is in focus in this column; geometry will most likely again follow soon.
As noted in an earlier column, from the viewpoint of automated reasoning and, in a different way, from the viewpoint of mathematics, when asked to find a proof for a theorem, you have three choices. You can proceed as is often done in a class by starting with the axioms, make one deduction after another, and conclude with the desired result. In other words, you can produce a forward proof. Instead, you could deny the conclusion of the theorem, work backward, and, if successful, produce a deduction that contradicts some axiom. In this case, you have a backward proof. Or, as you have surmised, you can seek a bidirectional proof, working forward from the axioms and backward from the denial of the conclusion.
I give you the following problem, from ring theory, to address.
Let a and b be elements of a ring such that a, b, and ab − 1 are units.
Show that a − b-1 is unit.
In OTTER notation, the hypotehsis and denial of conclusion are the following.
a * inv(a) = 1. b * inv(b) = 1. (a*b + m(1)) * inv(a*b + m(1)) = 1. % negated goal (a + m(inv(b))) * x != 1. x = x. % Ring axioms 0 + x = x. x + 0 = x. m(x) + x = 0. x + m(x) = 0. (x + y) + z = x + (y + z). x + y = y + x. (x * y) * z = x * (y * z). x * (y + z) = (x * y) + (x * z). (y + z) * x = (y * x) + (z * x). % a multiplicative unit x * 1 = x. 1 * x = x.
You are first challenged to find a proof, any proof.
Then, perhaps more challenging, you are asked to find a forward proof.
for his pioneering contributions to theorem proving and program verification, such as his seminal work with Derek Oppen on the combination of satisfiability procedures and fast congruence closure algorithms, the development of the highly influential theorem prover Simplify, and his role in the creation of the field of extended static checking.
The Award will be presented at CADE 24, the 24th International Conference on Automated Deduction.
The Woody Bledsoe Student Travel Award was created to honor the memory of Woody Bledsoe, for his contributions to mathematics, artificial intelligence, and automated theorem proving, and for his dedication to students. The award is intended to enable selected students to attend the International Conference on Automated Deduction (CADE) or the International Joint Conference on Automated Reasoning (IJCAR), whichever is scheduled for the year, by covering part of their expenses.
In 2013, CADE will take place from June 9 through June 14, in Lake Placid, New York, USA (for further information see the CADE web page). The winners will be partially reimbursed (e.g., between USD 200 and USD 750) for their conference registration, transportation, and accomodation expenses. Preference will be given to students who will play an active role in the conference, including satellite workshops, and do not have alternative funding. However, also students in other situations are very much encouraged to apply.
A nomination consists of a recommendation letter of up to 300 words from the student’s advisor. Nominations for CADE-24 should be sent by e-mail to
Maria Paola Bonacina, CADE-24 Program Chair (mariapaola.bonacina (at) univr.it)
and
Christopher A. Lynch and Neil V. Murray, CADE-24 Conference Chairs (clynch (at) clarkson.edu and nvm (at) cs.albany.edu)
Nominations must arrive no later than May 2, 2013. The selection will be made by the Chairs together with the Program Committee and the winners will be notified by May 9, 2013.
The awards will be presented at CADE-24; in case a winner does not attend, the chairs may transfer the award to another nominee or give no award.
The 24th International Conference on Automated Deduction will take place in Lake Placid, NY, USA, on 9–14 June 2013.
The deadline for early registration is 22 May 2013.
CADE is the major forum for the presentation of research in all aspects of automated deduction. CADE-24 is held in Lake Placid, a charming village on the shore of two lakes surrounded by the beautiful Adirondacks Mountains, upstate New York.
The conference program features:
IMPORTANT DATES:
Early registration deadline: 22 May 2013
Workshops and Tutorials: 9-10 June 2013
Conference: 11-14 June 2013
CASC: 12 June 2013
Please refer to the conference web site for further information.
FroCoS 2013, the 9th International Symposium on Frontiers of Combining Systems will take place in Nancy, France, on 18–20 September 2013. FroCos will be co-located with TABLEAUX 2013, the 22nd conference on AR with Analytic Tableaux and Related methods.
In various areas of computer science, such as logic, computation, program development and verification, artificial intelligence, knowledge representation and automated reasoning, there is an obvious need for using specialised formalisms and inference mechanisms for special tasks. In order to be usable in practice, these specialised systems must be combined with each other, and they must be integrated into general purpose systems.
Like its predecessors, FroCoS 2013 seeks to offer a common forum for research in the general area of combination, modularization and integration of systems, with emphasis on logic-based ones, and of their practical use.
Research papers of up to 16 pages are to be submitted until 22 April 2013, with abstracts due on 15 April. Please refer to the conference web site for full details, including submission information.
LPAR-19, the 19th International Conference on Logic for Programming, Artificial Intelligence and Reasoning will take place in Stellenbosch, South Africa, 14–19 December 2013. New results in the fields of computational logic and applications are welcome. Also welcome are more exploratory presentations, which may examine open questions and raise fundamental concerns about existing theories and practices. Topics of interest include, but are not limited to:
|
|
The deadline for paper submission is 2 August, with abstracts due on 22 July.
LPAR-19 also calls for workshop proposals. Workshops will be held on 14th December either as one-day or half-day events. If you would like to propose a workshop for LPAR-19, please contact the workshop chair via email (lkovacs (at) complang.tuwien.ac.at), until 15 July.
Please refer to the conference web page for more information.
The 19th Meeting on Types for Proofs and Programs will take place in Toulouse, France on 22–26 April 2013.
The Types Meeting is a forum to present new and on-going work in all aspects of type theory and its applications, especially in formalized and computer assisted reasoning and computer programming.
Invited Speakers:
34 contributed talks were selected by the program committee (main conference: morning of April 23 to midday of April 26).
Please register here.
Satellite events:
All the details are accessible through the main web site of TYPES 2013.
The 15th International Symposium on Symbolic and Numeric Algorithms for Scientific Computing (SYNASC 2013)
will take place in Timisoara, Romania, on 23–26 September 2013.
SYNASC aims to stimulate the interaction between the two scientific communities of symbolic and numeric computing and to exhibit interesting applications of the areas both in theory and in practice. Symbolic computing is here taken in a broad sense, to include computational logic, theorem proving, formal verification, etc. The choice of the topic is motivated by the belief of the organizers that the dialogue between the two communities is very necessary for accelerating the progress in making the computer a truly intelligent aid for mathematicians and engineers.
Proposals for Workshops, Tutorials, and Special Sessions are invited until 7 April 2013. Research papers are to be submitted until 26 May 2013, with abstracts due on 19 May.
Please refer to the Symposium Web Page for further details.
The Research Institute for Symbolic Computation (RISC) offers positions and fellowships for doctoral studies in symbolic computation.
The Research Institute for Symbolic Computation (RISC) in the castle of Hagenberg, Austria, is an international institute with its research focus on various branches of symbolic computation. Research interests of RISC include
RISC seeks applications of excellent and highly motivated students with a university degree in mathematics and/or computer science. Experience in symbolic computation is an advantage but no formal requirement.
More information is available from the web site of the PhD programme.
Doctoral Student Positions in Information and Communication Technologies on the research project “Advanced SMT Techniques for Word-level Formal Verification - (WOLF)” are available at the International Doctorate School in Information and Communication Technologies of the University of Trento, Italy, under the joint supervision of Alessandro Cimatti, FBK, Trento, and Roberto Sebastiani, DISI, University of Trento.
The research activity will be carried out jointly within the Embedded Systems (ES) Research Unit of the Center for Scientific and Technological Research of the Fondazione Bruno Kessler (FBK), Trento, and the Software Engineering & Formal Methods (SE&FM) Research Program, at Department of Information Engineering and Computer Science (DISI) of University of Trento.
The research activity will aim at investigating and developing novel techniques, methodologies and support tools for Satisfiability Modulo Theories (SMT) for the formal verification of systems. This work will be part of the "Advanced SMT Techniques for Word-level Formal Verification - (WOLF)" project, a three-year research project supported by SRC/GRC, in strict collaboration with the Formal Verification Group at Intel, Haifa, and other major HW companies.
The goal of the WOLF project is to provide a comprehensive SMT package to support effective formal verification of systems ranging from RTL circuits all the way up to high-level hardware description languages (e.g. SystemC) and software. The package will be implemented on top of the MathSAT.5 SMT platform (http://mathsat.fbk.eu/), and provided as an API.
Ph.D. courses will start in Autumn 2013, and the thesis must be completed in three or four years. People enrolled Ph.D. courses are expected to move to Trento, and will receive monetary support during phases of their activity.
Interested candidates should inquire for further information and/or apply by sending email to wolf-recruit (at) disi.unitn.it
Applications should contain a statement of interest, with a Curriculum Vitae, and three reference persons. PDF format is strongly encouraged.
Emails will be automatically processed and should have 'PHD ON WOLF PROJECT' as subject.
Contact Person: Prof. ROBERTO SEBASTIANI (rseba[at]disi[dot]unitn[dot]it)
Since 2002, FoLLI (the Association for Logic, Language, and Information, ) awards the E.W. Beth Dissertation Prizeto outstanding dissertations in the fields of Logic, Language, and Information. We invite submissions for the best dissertation which resulted in a Ph.D. degree in the year 2012. The dissertations will be judged on technical depth and strength, originality, and impact made in at least two of three
fields of Logic, Language, and Computation. Interdisciplinarity is an impor
tant feature of the theses competing for the E.W. Beth Dissertation Prize.
Who qualifies. Nominations of candidates are admitted who were awarded a Ph.D. degree in the areas of Logic, Language, or Information between January 1st, 2012 and December 31st, 2012. There is no restriction on the nationality of the candidate or the university where the Ph.D. was granted. After a careful consideration, FoLLI has decided to accept only dissertations written in English. Dissertations produced in 2012 but not written in English or not translated will be allowed for submission, after translation, also with the call next year (for dissertations defended in 2013). The present call for nominations for the E.W. Beth Disertation Award 2013 will also accept nominations of full English translations of theses originally written in another language than English and defended in 2011 or 2012.
The prize consists of:
How to submit. Only electronic submissions are accepted. The following documents are required:
All documents must be submitted electronically (preferably as a zip file) to buszko (at) amu.edu.pl. Hard copy submissions are not admitted. In case of any
problems with the email submission or a lack of notification within three
working days, nominators should write to buszko (at) amu.edu.pl.
Important dates:
Deadline for Submissions: May 12, 2013.
Notification of Decision: July 14, 2013.
Mutually-inversistic logic deems that the truth table for material implication cannot be used to make hypothetical inference but its inverse functions can. Mutually-inversistic logic includes two calculi and four theories.
Mutually-inversistic mathematics includes algebra, geometry, and analysis.
In rule-based systems, a rule is both an inference rule and a tautology. In mutually-inversistic automated decomposition systems, a rule is either an inference rule or a tautology but not both, especially hypothetical syllogism is a tautology but not an inference rule. In this way, reasoning can be made automated. Mutually-inversistic automated decomposition systems include an automated theorem prover for hardware verification and mutually-inversistic program verification.
My monograph entitled “Mutually-inversistic logic, mathematics, and their applications” has been published by Central Compilation & Translation Press. It contains a discussion of automated reasoning for mutually-inversistic logic.