@inproceedings{abdollahzadeh-barforoush02__oav_vvt_exper_integ_verif_,
 title        = {OAV-VVT Expert Integrated Verification and Validation Tool For Knowledge Base System},
 author       = {Abdollahzadeh-Barforoush, Ahmad and Dadhkah, Chitra},
 year         = {2002},
 tags         = {},
 pages        = {2-3},
 crossref     = {walsh02:_proceed_works_autom_reason_},
}

@inproceedings{anderson02__solut_to_probl_of_contr_,
 title        = {A Solution To The Problem Of Contradiction In Knowledge Discovery Applications},
 author       = {Anderson, David},
 year         = {2002},
 tags         = {},
 pages        = {4},
 crossref     = {walsh02:_proceed_works_autom_reason_},
}

@inproceedings{basukoski02__towar_autom_gener_of_belief_,
 title        = {Towards Automated Generation Of Beliefs In BDI Agents},
 author       = {Basukoski, A. and Bolotov, Alexander},
 year         = {2002},
 tags         = {},
 pages        = {5-6},
 crossref     = {walsh02:_proceed_works_autom_reason_},
}

@inproceedings{benzmueller02_,
 title        = {Agent-Based Theorem Proving},
 author       = {Benzmüller, Christoph and Sorge, Volker},
 year         = {2002},
 tags         = {},
 pages        = {7-8},
 crossref     = {walsh02:_proceed_works_autom_reason_},
}

@inproceedings{chubarov02__solvin_multip_contain_tests_for_,
 title        = {Solving Multiple Containment Tests For Linear Constraints Over Integers},
 author       = {Chubarov, Dmitri and Voronkov, Andrei},
 year         = {2002},
 tags         = {},
 pages        = {9-10},
 crossref     = {walsh02:_proceed_works_autom_reason_},
}

@inproceedings{ciortuz02__learn_typed_unific_gramm_,
 title        = {On Learning Typed-Unification Grammars},
 author       = {Ciortuz, Liviu},
 year         = {2002},
 tags         = {},
 pages        = {11-12},
 crossref     = {walsh02:_proceed_works_autom_reason_},
}

@inproceedings{colton02__semi_autom_discov_in_zaris_spaces_propos_,
 title        = {Semi-Automated Discovery In Zariski Spaces (A Proposal)},
 author       = {Colton, Simon and McCasland, Roy and Bundy, Alan and Walsh, Toby},
 year         = {2002},
 tags         = {},
 pages        = {13-14},
 crossref     = {walsh02:_proceed_works_autom_reason_},
}

@inproceedings{dennis02__plann_whisk_probl_,
 title        = {Planning The Whiskey Problem},
 author       = {Dennis, Louise A. and Bundy, Alan},
 year         = {2002},
 tags         = {},
 pages        = {15-16},
 crossref     = {walsh02:_proceed_works_autom_reason_},
}

@inproceedings{dixon02__relat_ebtween_tempor_logic_normal_,
 title        = {The Relationship Ebtween Temporal Logic Normal Forms And Alternating Automata},
 author       = {Dixon, Clare and Bolotov, Alexander and Fisher, Michael},
 year         = {2002},
 tags         = {},
 pages        = {17-18},
 crossref     = {walsh02:_proceed_works_autom_reason_},
}

@inproceedings{drake02__compar_sat_prepr_techn_,
 title        = {Comparing SAT Preprocessing Techniques},
 author       = {Drake, Lyndon and Frisch, Alan},
 year         = {2002},
 tags         = {},
 pages        = {19-20},
 crossref     = {walsh02:_proceed_works_autom_reason_},
}

@inproceedings{endriss02__addin_zoom_to_linear_tempor_logic_,
 title        = {Adding A Zoom To Linear Temporal Logic},
 author       = {Endriss, Ulrich},
 year         = {2002},
 tags         = {},
 pages        = {21-22},
 crossref     = {walsh02:_proceed_works_autom_reason_},
}

@inproceedings{frisch02__autom_trans_const_satis_probl_,
 title        = {Automatically Transforming Constraint Satisfaction Problems},
 subtitle     = {Further Progress},
 author       = {Frisch, Alan M. and Miguel, Ian and Walsh, Toby},
 year         = {2002},
 tags         = {},
 pages        = {23-24},
 crossref     = {walsh02:_proceed_works_autom_reason_},
}

@inproceedings{gago02__algor_for_guidin_claus_tempor_resol_,
 title        = {Algorithms For Guiding Clausal Temporal Resolution},
 author       = {Gago, M. Carmen Fernández},
 year         = {2002},
 tags         = {},
 pages        = {25-26},
 crossref     = {walsh02:_proceed_works_autom_reason_},
}

@inproceedings{georgieva02__relat_between_decid_fragem_non_,
 title        = {On The Relationship Between Decidable Fragemtns, Non-Classical Logics, And Description Logics},
 author       = {Georgieva, Lilia and Hustadt, Ulrich and Schmidt, Renate A.},
 year         = {2002},
 tags         = {},
 pages        = {27-28},
 crossref     = {walsh02:_proceed_works_autom_reason_},
}

@inproceedings{hazarika02__using_spass_for_provin_theor_within_mereot_,
 title        = {Using SPASS For Proving Theorems Within Mereotopology},
 author       = {Hazarika, Shyamanta M. and Cohn, Anthony G.},
 year         = {2002},
 tags         = {},
 pages        = {29-30},
 crossref     = {walsh02:_proceed_works_autom_reason_},
}

@inproceedings{hurd02__fast_normal_in_hol_theor_prover_,
 title        = {Fast Normalization In The HOL Theorem Prover},
 author       = {Hurd, Joe},
 year         = {2002},
 tags         = {},
 pages        = {31-32},
 crossref     = {walsh02:_proceed_works_autom_reason_},
}

@inproceedings{ireland02__inves_into_proof_autom_for_,
 title        = {An Investigation Into Proof Automation For The SPARK Approach To High Integrity Ada},
 author       = {Ireland, Andrew and Ellis, Bill J. and Richardson, Julian},
 year         = {2002},
 tags         = {},
 pages        = {33},
 crossref     = {walsh02:_proceed_works_autom_reason_},
}

@inproceedings{jamnik02__autom_learn_of_proof_method_,
 title        = {Automatic Learning Of Proof Methods In Proof Planning},
 author       = {Jamnik, Mateja and Kerber, Manfred and Pollet, Martin and Benzmüller, Christoph},
 year         = {2002},
 tags         = {},
 pages        = {34-35},
 crossref     = {walsh02:_proceed_works_autom_reason_},
}

@inproceedings{konev02__trp_,
 title        = {TRP++},
 subtitle     = {Implementation Of Clausal Resolution For Propositional Linear-Time Temporal Logic},
 author       = {Konev, Boris},
 year         = {2002},
 tags         = {},
 pages        = {36-37},
 crossref     = {walsh02:_proceed_works_autom_reason_},
}

@inproceedings{kontchakov02__tempor_tableaux_,
 title        = {Temporalising Tableaux},
 author       = {Kontchakov, Roman and Lutz, Carsten and Wolter, Frank and Zakharyaschev, Michael},
 year         = {2002},
 tags         = {},
 pages        = {38-39},
 crossref     = {walsh02:_proceed_works_autom_reason_},
}

@inproceedings{korovin02__decid_of_first_order_theor_,
 title        = {The Decidability Of The First-Order Theory Of The Knuth-Bendix Orders In The Case Of Unary Signatures},
 author       = {Korovin, Konstantin and Voronkov, Andrei},
 year         = {2002},
 tags         = {},
 pages        = {40-41},
 crossref     = {walsh02:_proceed_works_autom_reason_},
}

@inproceedings{meisel02__concep_,
 title        = {CONCEPTOOL},
 subtitle     = {Intelligent Support To Knowledge Management},
 author       = {Meisel, Helmut and Compatangelo, Ernesto},
 year         = {2002},
 tags         = {},
 pages        = {42-43},
 crossref     = {walsh02:_proceed_works_autom_reason_},
}

@inproceedings{metcalfe02__hyers_calcul_for_abelian_logic_,
 title        = {A Hypersequent Calculus For Abelian Logic},
 author       = {Metcalfe, George},
 year         = {2002},
 tags         = {},
 pages        = {44-45},
 crossref     = {walsh02:_proceed_works_autom_reason_},
}

@inproceedings{nalon02__resol_for_tempor_logic_of_,
 title        = {Resolution For Temporal Logics Of Knowledge With Interactions},
 author       = {Nalon, Cláudia and Dixon, Clare and Fischer, Michael},
 year         = {2002},
 tags         = {},
 pages        = {46-47},
 crossref     = {walsh02:_proceed_works_autom_reason_},
}

@inproceedings{pease02__lakat_style_reason_,
 title        = {Lakatos-Style Reasoning},
 author       = {Pease, Alison and Colton, Simon and Smaill, Alan and Lee, John},
 year         = {2002},
 tags         = {},
 pages        = {48-49},
 crossref     = {walsh02:_proceed_works_autom_reason_},
}

@inproceedings{piroi02__inter_provin_in_theor_,
 title        = {Interactive Proving In Theorema},
 author       = {Piroi, Florina and Jebelean, Tudor},
 year         = {2002},
 tags         = {},
 pages        = {50-51},
 crossref     = {walsh02:_proceed_works_autom_reason_},
}

@inproceedings{ramsay02__using_chart_to_recor_inter_,
 title        = {Using A Chart To Record Intermediate Results In A Model Generation Theorem Prover},
 author       = {Ramsay, Allan},
 year         = {2002},
 tags         = {},
 pages        = {52-55},
 crossref     = {walsh02:_proceed_works_autom_reason_},
}

@inproceedings{rybina02__brain_,
 title        = {BRAIN},
 subtitle     = {Backward Reachability Analysis With INtegers},
 author       = {Rybina, Tatiana and Voronkov, Andrei},
 year         = {2002},
 tags         = {},
 pages        = {56-58},
 crossref     = {walsh02:_proceed_works_autom_reason_},
}

@inproceedings{schmidt02__subst_test_knowl_in_axiom_,
 title        = {Substitutions, Test and Knowledge In Axiomatic Products Of PDL and S5},
 author       = {Schmidt, Renate A. and Tishkovsky, Dmitry},
 year         = {2002},
 tags         = {},
 pages        = {59-60},
 crossref     = {walsh02:_proceed_works_autom_reason_},
}

@inproceedings{smaill02__proof_plann_diagon_theor_via_categ_theor_,
 title        = {Proof Planning Diagonalisation Theorems Via Category Theory},
 author       = {Smaill, Alan},
 year         = {2002},
 tags         = {},
 pages        = {61-62},
 crossref     = {walsh02:_proceed_works_autom_reason_},
}

@inproceedings{steel02__using_implic_induc_to_guide_,
 title        = {Using Implict Induction To Guide A Parallel Search For Inconsistency},
 author       = {Steel, Graham and Bundy, Alan and Denney, Ewen},
 year         = {2002},
 tags         = {},
 pages        = {63-64},
 crossref     = {walsh02:_proceed_works_autom_reason_},
}

@inproceedings{torrini02__embed_quanit_logic_for_spatial_,
 title        = {Embedding A Quanitifed Logic For Spatial Reasoning In Isabelle-HOL},
 author       = {Torrini, Paolo and Fleuriot, Jacques D. and Stell, John G. and Bennett, Brandon},
 year         = {2002},
 tags         = {},
 pages        = {65-66},
 crossref     = {walsh02:_proceed_works_autom_reason_},
}

@proceedings{walsh02:_proceed_works_autom_reason_,
 title        = {Proceedings of the 9th Workshop on Automated Reasoning},
 subtitle     = {Bridging the Gap between Theory and Practice},
 editor       = {Walsh, Toby},
 year         = {2002},
 tags         = {},
 address      = {Imperial College London, UK},
 pdf_locked   = {False},
 url          = {https://aisb.org.uk/wp-content/uploads/2019/12/AISB02_ARW.pdf},
 url2         = {https://web.archive.org/web/20190115201026/http://www.aisb.org.uk/convention/aisb02/index.html},
 file         = {/media/john/data/todo/pdfs/proceedings/aisb/aisb_02/AISB02_ARW.pdf},
}