| Hyper tableaux P Baumgartner, U Furbach, I Niemelä European Workshop on Logics in Artificial Intelligence, 1-17, 1996 | 270 | 1996 |
| The model evolution calculus P Baumgartner, C Tinelli Automated Deduction–CADE-19: 19th International Conference on Automated …, 2003 | 123 | 2003 |
| Protein: A PROver with a Theory Extension INterface P Baumgartner, U Furbach International Conference on Automated Deduction, 769-773, 1994 | 104 | 1994 |
| Computing finite models by reduction to function-free clause logic P Baumgartner, A Fuchs, H De Nivelle, C Tinelli Journal of Applied Logic 7 (1), 58-74, 2009 | 96 | 2009 |
| FDPLL—a first-order Davis-Putnam-Logeman-Loveland procedure P Baumgartner Automated Deduction-CADE-17: 17th International Conference on Automated …, 2000 | 96 | 2000 |
| Hyper tableau—the next generation P Baumgartner International Conference on Automated Reasoning with Analytic Tableaux and …, 1998 | 94 | 1998 |
| The TPTP typed first-order form with arithmetic G Sutcliffe, S Schulz, K Claessen, P Baumgartner Logic for Programming, Artificial Intelligence, and Reasoning: 18th …, 2012 | 92 | 2012 |
| Implementing the model evolution calculus P Baumgartner, A Fuchs, C Tinelli International Journal on Artificial Intelligence Tools 15 (01), 21-52, 2006 | 83 | 2006 |
| Hierarchic superposition with weak abstraction P Baumgartner, U Waldmann Automated Deduction–CADE-24: 24th International Conference on Automated …, 2013 | 67 | 2013 |
| A novel architecture for situation awareness systems F Baader, A Bauer, P Baumgartner, A Cregan, A Gabaldon, K Ji, K Lee, ... Automated Reasoning with Analytic Tableaux and Related Methods: 18th …, 2009 | 58 | 2009 |
| Semantically guided theorem proving for diagnosis applications P Baumgartner, P Fröhlich, U Furbach, W Nejdl IJCAI (1), 460-465, 1997 | 53 | 1997 |
| Blocking and other enhancements for bottom-up model generation methods P Baumgartner, RA Schmidt International Joint Conference on Automated Reasoning, 125-139, 2006 | 52 | 2006 |
| Model Elimination without Contrapositives and its Application to PTTP P Baumgartner, U Furbach Journal of automated reasoning 13, 339-359, 1994 | 52 | 1994 |
| The model evolution calculus as a first-order DPLL method P Baumgartner, C Tinelli Artificial Intelligence 172 (4-5), 591-632, 2008 | 51 | 2008 |
| Darwin: A theorem prover for the model evolution calculus P Baumgartner, A Fuchs, C Tinelli IJCAR Workshop on Empirically Successful First Order Reasoning (ESFOR (aka …, 2004 | 45 | 2004 |
| The Taming of the (X) OR P Baumgartner, F Massacci Computational Logic—CL 2000: First International Conference London, UK …, 2000 | 45 | 2000 |
| Hyper tableaux with equality P Baumgartner, U Furbach, B Pelzer International Conference on Automated Deduction, 492-507, 2007 | 43 | 2007 |
| Lemma learning in the model evolution calculus P Baumgartner, A Fuchs, C Tinelli International Conference on Logic for Programming Artificial Intelligence …, 2006 | 39 | 2006 |
| The model evolution calculus with equality P Baumgartner, C Tinelli International Conference on Automated Deduction, 392-408, 2005 | 39 | 2005 |
| A confluent connection calculus H Ganzinger, P Baumgartner, N Eisinger, U Furbach Automated Deduction—CADE-16: 16th International Conference on Automated …, 1999 | 38 | 1999 |
Cesare TinelliProfessor of Computer Science, The University of Iowa在 uiowa.edu 的电子邮件经过验证
