COOKIES: By using this website you agree that we can place Google Analytics Cookies on your device for performance monitoring. |

University of Cambridge > Talks.cam > Computer Laboratory Automated Reasoning Group Lunches > From QED to X-Logic, following the lead of Leibniz

## From QED to X-Logic, following the lead of LeibnizAdd to your list(s) Download to your calendar using vCal - Roger Bishop Jones (None)
- Tuesday 12 June 2007, 13:00-14:00
- Computer Laboratory, William Gates Building, Room GS15.
If you have a question about this talk, please contact Thomas Tuerk. Was the QED project for the formalisation of mathematics too ambitious? Leibniz, whose conception of a universal language and calculus of reasoning preceded QED by 300 years, would have thought it faint-hearted, the two most difficult problems in realising his grander vision having been resolved by the revolution in modern logic and the invention of the electronic digital computer. “X-Logic” is a contemporary interpretation of Leibniz’s project. Like the original, it is a multi-disciplinary enterprise, straddling the boundaries between philosophy, logic, computing, and science. In this talk after introducing Leibniz and his project, I will enumerate some philosophical principles endemic to the Cambridge Automated Reasoning Group (implicit in the methods and/or explicit in some of the publications of the ARG ). Some consequences of these philosophical principles for an architecture for globally distributed, linguistically pluralistic, automated deduction will then be considered, making use of a formal model in Isabelle-HOL. At this level inference takes place between documents, which are understood as complex propositions, and may be in any language which has a well-defined abstract semantics. The notion of proof is generalised to encompass all correct computation relative to program specifications expressed in terms of the languages of documents. Assurance of the truth of propositions thus proven is managed by the qualification of judgements with a list of those authorities upon whose infallibility certainty in the content of the judgement rests. A central concern is the articulation of a notion of soundness appropriate to this context. A manner of resolving the foundational problem of semantic regress, and that of a final resort on matters of consistency. will be touched upon. This talk is part of the Computer Laboratory Automated Reasoning Group Lunches series. ## This talk is included in these lists:- All Talks (aka the CURE list)
- Cambridge talks
- Computer Laboratory Automated Reasoning Group Lunches
- Computer Laboratory talks
- Computer Laboratory, William Gates Building, Room GS15
- Interested Talks
- School of Technology
- Trust & Technology Initiative - interesting events
- bld31
- yk373's list
Note that ex-directory lists are not shown. |
## Other listsEvolutionary Genetics Journal Club Judge Business Club Financial Economcs Series Centre for European Legal Studies## Other talksAccess to Medicines Imaging techniques and novel tools for early detection and intervention New methods for genetic analysis The Age of the Applied Economist: The Transformation of Economics Since the 1970s Modelling seasonal acceleration of land terminating sectors of the Greenland Ice Sheet margin |