BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//Talks.cam//talks.cam.ac.uk//
X-WR-CALNAME:Talks.cam
BEGIN:VEVENT
SUMMARY:From QED to X-Logic\, following the lead of Leibniz - Roger Bishop
  Jones (None)
DTSTART:20070612T120000Z
DTEND:20070612T130000Z
UID:TALK7415@talks.cam.ac.uk
CONTACT:Thomas Tuerk
DESCRIPTION:Was the QED project for the formalisation of mathematics too a
 mbitious? Leibniz\, whose conception of a universal language and calculus 
 of reasoning preceded QED by 300 years\, would have thought it faint-heart
 ed\, the two most difficult problems in realising his grander vision havin
 g been resolved by the revolution in modern logic and the invention of the
  electronic digital computer.\n\n"X-Logic" is a contemporary interpretatio
 n of Leibniz's project. Like the original\, it is a multi-disciplinary ent
 erprise\, straddling the boundaries between philosophy\, logic\, computing
 \, and science.\n\nIn 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\nof the ARG). Some consequences of these philosophica
 l principles for an architecture for globally distributed\, linguistically
  pluralistic\, automated deduction\nwill then be considered\, making use o
 f a formal model in Isabelle-HOL.\n\nAt this level inference takes place b
 etween 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\nto 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 quali
 fication of judgements\nwith a list of those authorities upon whose infall
 ibility certainty in the content of the judgement rests.\n\nA central conc
 ern is the articulation of a notion of soundness appropriate to this conte
 xt. A manner of resolving the foundational problem of semantic\nregress\, 
 and that of a final resort on matters of consistency. will be touched upon
 .
LOCATION:Computer Laboratory\, William Gates Building\, Room GS15
END:VEVENT
END:VCALENDAR