ARW 2002 Proceedings -- Table of Contents ***************************************** 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 Christoph Benzmuller and Volker Sorge, Unviersities of the Saarlandes and Birmingham Agent-Based Theorem Proving Dmitri Chubarov and Andrei Voronkov, University of Manchester Solving Multiple Containment Tests for Linear Constraints over Integers Liviu Ciortuz, Univeristy of York On learning typed-unification grammars Simon Colton, Roy McCasland, Alan Bundy and Toby Walsh, University of Edinburgh Semi-Automated Discovery in Zariski Spaces (A Proposal) Louis Dennis and Alan Bundy, Universities of Nottingham and Edinburgh Planning the Whisky Problem Clare Dixon, Alexander Bolotov and Michael Fisher, Universities of Liverpool and Westminster The Relationship Between Temporal Logic Normal Forms and Alternating Automata Lyndon Drake, Alan Frisch, Ines Lynce, Joao Marques-Silva and Toby Walsh University of York and INESC, Portugal Comparing SAT preprocessing techniques Ulrich Endriss, King's College London Adding a Zoom to Linear Temporal Logic Alan Frisch, Ian Miguel and Toby Walsh, University of York Automatically Trasnforming Constraint Satisfaction Problems: Further Progress Edmund Furse, Imitation Ltd Programming by Immitation M. Carmen Fernandez Gago, University of Liverpool Algorithms for Guiding Clausal Temporal Resolution Lilia Georgieva, Ullrich Hustadt and Renate Schmidt, Universities of Manchester and Liverpool On the relationship between decidable fragments, non-classical logics and description logics Shyamanta M Hazarika and Anthony G Cohn, University of Leeds Using SPASS for proving theorems in Mereotopology Joe Hurd, University of Cambridge Fast Normalization in the HOL Theorem Prover Andrew Ireland, Bill Ellis and Julian Richardson, Heriot-Watt University An Investigation into Proof Automation for the SPARK Approach to High Integrity Ada Mateja Jamnik, Manfred Kerber, Martin Pollet and Christoph Benzmuller, Universities of Birmingham and the Saarlandes Automatic Learning of Proof Methods in Proof Planning Boris Konev, University of Liverpool TRP++: Implementation of Clausal Resolution for Propositioanl Linear-Time Temporal Logic 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 H. Meisel and E. Compatangelo, University of Aberdeen ConcepTool: Intelligent Support to Knowledge Management George Metcalfe, King's College London A hypersequent calculus for Abelian Logic Claudia Nalon, Clare Dixon and Michael Fisher, University of Liverpool Resolution for Temporal Logics of Knowledge with Interactions Alison Pease, Simon Colton, Alan Smaill and John Lee, University of Edinburgh Lakatos-style Reasoning Florina Piroi and Tudo Jebelena, RISC, Austria Interactive Proving in Theorema Allan Ramsay, UMIST Using a chart to record intermediate results in a model generation theorem prover Tatiana Rybina and Andrei Voronkov, University of Manchester BRAIN: Backward Reachability Analysis with INtegers Renate Schmidt and Dmitry Tishkovsky, University of Manchester Subsitutions, test and knowledge in axiomatic products of PDL and S5 Alan Smaill, University of Edinburgh Proof Planning Diagonalization Theorems via Category Theory Graham Steel, Alan Bundy, and Ewen Denney, University of Edinburgh Using Implicit Induction to Guide a Parallel Search for Inconsistency Paolo Torrini, Jacques Fleuriot, John Stell, and Brandon Bennet, Universities of Leeds and Edinburgh Embedding a quantified logic for spatial reasoning in Isabelle-HOL