ARW 2002 Programme ================== Wed 3rd April 09.00 Registration opens 10.00-11.00 Invited talk Colin O'Halloran (QinetiQ) Challenges and benefits of verification for certification 11.00-11.30 Coffee 11.30-12.45 Poster session (I) Joe Hurd, University of Cambridge Fast Normalization in the HOL Theorem Prover Tatiana Rybina and Andrei Voronkov, University of Manchester BRAIN: Backward Reachability Analysis with INtegers Dmitri Chubarov and Andrei Voronkov, University of Manchester Solving Multiple Containment Tests for Linear Constraints over Integers Lyndon Drake, Alan Frisch, Ines Lynce, Joao Marques-Silva and Toby Walsh University of York and INESC, Portugal Comparing SAT preprocessing techniques Dan Sheridan, Alan Frisch and Toby Walsh University of York Bounded Model Checking Boris Konev, University of Liverpool TRP++: Implementation of Clausal Resolution for Propositioanl Linear-Time Temporal Logic M. Carmen Fernandez Gago, University of Liverpool Algorithms for Guiding Clausal Temporal Resolution Ulrich Endriss, King's College London Adding a Zoom to Linear Temporal Logic 12.45-14.00 Lunch 14.00-15.00 ARW/AISB Invited talk Ian Horrocks (University of Manchester) DAML+OIL: a Reason-able Ontology Language for the Semantic Web 15.00-16.00 Posters (II) Alison Pease, Simon Colton, Alan Smaill and John Lee, University of Edinburgh Lakatos-style Reasoning Simon Colton, Roy McCasland, Alan Bundy and Toby Walsh, University of Edinburgh Semi-Automated Discovery in Zariski Spaces (A Proposal) Mateja Jamnik, Manfred Kerber, Martin Pollet and Christoph Benzmuller, Universities of Birmingham and the Saarlandes Automatic Learning of Proof Methods in Proof Planning Louis Dennis and Alan Bundy, Universities of Nottingham and Edinburgh Planning the Whisky Problem Alan Smaill, University of Edinburgh Proof Planning Diagonalization Theorems via Category Theory Alan Frisch, Ian Miguel and Toby Walsh, University of York Automatically Trasnforming Constraint Satisfaction Problems: Further Progress 16.00-16.30 Coffee 16.30-17.45 Posters (III) Graham Steel, Alan Bundy, and Ewen Denney, University of Edinburgh Using Implicit Induction to Guide a Parallel Search for Inconsistency Shyamanta M Hazarika and Anthony G Cohn, University of Leeds Using SPASS for proving theorems in Mereotopology H. Meisel and E. Compatangelo, University of Aberdeen ConcepTool: Intelligent Support to Knowledge Management Allan Ramsay, UMIST Using a chart to record intermediate results in a model generation theorem prover A.-B. Ahmad and D. Chitra, Amirkabir University of Technology, Tehran OAV-VVT Expert Integrated Verification and Validation Tool For Knowledge Base Systems David Anderson, University of Portsmouth A solution to the problem of contradiction in knowledge discovery applications A. Basukoski and A. Bolotov, University of Westminster, Towards automated generation of beliefs in BDI agents 19.00- Workshop dinner Soraya Restaurant, http://www.sorayarestaurant.com/ Thurs 4th April 09.00-10.00 Invited talk John Harrison (Intel Corporation) Theorem Proving in Real Applications 10.00-10.45 Demos Edmund Furse, Imitation Ltd Programming by Immitation Florina Piroi and Tudo Jebelena, RISC, Austria Interactive Proving in Theorema 10.45-11.15 Coffee 11.15-13.00 Posters (IV) Christoph Benzmuller and Volker Sorge, Unviersities of the Saarlandes and Birmingham Agent-Based Theorem Proving Lilia Georgieva, Ullrich Hustadt and Renate Schmidt, Universities of Manchester and Liverpool On the relationship between decidable fragments, non-classical logics and description logics Clare Dixon, Alexander Bolotov and Michael Fisher, Universities of Liverpool and Westminster The Relationship Between Temporal Logic Normal Forms and Alternating Automata Claudia Nalon, Clare Dixon and Michael Fisher, University of Liverpool Resolution for Temporal Logics of Knowledge with Interactions Roman Kontchakov, Carsten Lutz, Frank Wolter and Michael Zakharyaschev, King's College London Temporalising tableaux Konstantin Korovin and Andrei Voronkov, University of Manchester The decidability of the first-order theory of the Knuth-Bendix orders in the case of unary signatures Renate Schmidt and Dmitry Tishkovsky, University of Manchester Subsitutions, test and knowledge in axiomatic products of PDL and S5 George Metcalfe, King's College London A hypersequent calculus for Abelian Logic Liviu Ciortuz, Univeristy of York On learning typed-unification grammars Paolo Torrini, Jacques Fleuriot, John Stell, and Brandon Bennet, Universities of Leeds and Edinburgh Embedding a quantified logic for spatial reasoning in Isabelle-HOL 13.00-14.15 Lunch Fri 5th April (optional) 13.30-14.30 AISB Plenary Stephen Muggleton Uncertainty, Logic and Learning