Edit Profile (opens in new tab) Paulson, Lawrence Charles Compute Distance To: Compute Author ID: paulson.lawrence-charles Published as: Paulson, Lawrence C.; Paulson, Lawrence; Paulson, Lawrence Charles; Paulson, Larry; Paulson, L. C. more...less Homepage: https://www.cl.cam.ac.uk/~lp15/ External Links: MGP · ORCID · Wikidata · Google Scholar · dblp · IdRef · theses.fr Documents Indexed: 90 Publications since 1983, including 5 Books 2 Contributions as Editor Co-Authors: 44 Co-Authors with 53 Joint Publications 649 Co-Co-Authors all top 5 Co-Authors 38 single-authored 6 Benzmüller, Christoph Ewald 5 Blanchette, Jasmin Christian 5 Li, Wenda 4 Akbarpour, Behzad 4 Bella, Giampaolo 4 Bridge, James P. 4 Meng, Jia 4 Nipkow, Tobias 3 Fleuriot, Jacques D. 3 Sultana, Nik 2 Abdulaziz, Mohammad 2 Ballarin, Clemens 2 Böhme, Sascha 2 Davenport, James Harold 2 England, Matthew 2 Holden, Sean B. 2 Huang, Zongyan 2 Koutsoukou-Argyraki, Angeliki 2 Massacci, Fabio 2 Passmore, Grant Olney 2 Theiss, Frank 2 Wenzel, Makarius 2 Wilson, David J. 1 Avigad, Jeremy 1 Bordg, Anthony 1 de Moura, Leonardo 1 de Vilhena, Paulo Emílio 1 Džamonja, Mirna 1 Edmonds, Chelsea 1 Ehmety, Sidi O. 1 Fietzke, Arnaud 1 Grabczewski, Krzysztof 1 Kaliszyk, Cezary 1 Kammüller, Florian 1 Kaufmann, Matt 1 Klein, Gerwin 1 Mangla, Chaitanya 1 Popescu, Andrei 1 Quigley, Claire 1 Snelting, Gregor 1 Susanto, Kong Woei 1 Tramontano, Piero 1 Urban, Josef 1 Wenzel, Markus all top 5 Serials 19 Journal of Automated Reasoning 3 Experimental Mathematics 3 Lecture Notes in Computer Science 2 Science of Computer Programming 2 Formal Aspects of Computing 2 Logic Journal of the IGPL 2 LMS Journal of Computation and Mathematics 2 ACM Transactions on Computational Logic 2 Journal of Applied Logic 1 The Computer Journal. Section A / Section B 1 The Journal of Logic Programming 1 Journal of Symbolic Computation 1 Information and Computation 1 Journal of Logic and Computation 1 MSCS. Mathematical Structures in Computer Science 1 The Bulletin of Symbolic Logic 1 Fundamenta Informaticae 1 Journal of Universal Computer Science 1 Cambridge Tracts in Theoretical Computer Science 1 Mathematics in Computer Science 1 Logica Universalis 1 The Review of Symbolic Logic 1 Journal of Formalized Reasoning 1 Proceedings of the Royal Society of London. A. Mathematical, Physical and Engineering Sciences all top 5 Fields 90 Computer science (68-XX) 38 Mathematical logic and foundations (03-XX) 5 Real functions (26-XX) 5 Information and communication theory, circuits (94-XX) 2 General and overarching topics; collections (00-XX) 2 History and biography (01-XX) 2 Functions of a complex variable (30-XX) 1 Combinatorics (05-XX) 1 Order, lattices, ordered algebraic structures (06-XX) 1 Number theory (11-XX) 1 Field theory and polynomials (12-XX) 1 Algebraic geometry (14-XX) 1 Category theory; homological algebra (18-XX) 1 Group theory and generalizations (20-XX) 1 Mechanics of particles and systems (70-XX) 1 Systems theory; control (93-XX) Publications by Year all cited Publications top 5 cited Publications Citations contained in zbMATH Open 71 Publications have been cited 1,236 times in 805 Documents Cited by ▼ Year ▼ Isabelle/HOL. A proof assistant for higher-order logic. Zbl 0994.68131Nipkow, Tobias; Paulson, Lawrence C.; Wenzel, Markus 396 2002 Isabelle. A generic theorem prover. Zbl 0825.68059Paulson, Lawrence C. 106 1994 The foundation of a generic theorem prover. Zbl 0679.68173Paulson, Lawrence C. 51 1989 ML for the working programmer. 2nd ed. Zbl 0863.68032Paulson, L. C. 43 1996 Extending Sledgehammer with SMT solvers. Zbl 1314.68272Blanchette, Jasmin Christian; Böhme, Sascha; Paulson, Lawrence C. 36 2013 Translating higher-order clauses to first-order clauses. Zbl 1203.68188Meng, Jia; Paulson, Lawrence C. 34 2008 MetiTarski: An automatic theorem prover for real-valued special functions. Zbl 1215.68206Akbarpour, Behzad; Paulson, Lawrence Charles 32 2010 LEO-II – a cooperative automatic theorem prover for classical higher-order logic. (System description). Zbl 1165.68446Benzmüller, Christoph; Paulson, Lawrence C.; Theiss, Frank; Fietzke, Arnaud 27 2008 Set theory for verification. I: From foundations to functions. Zbl 0802.68128Paulson, Lawrence C. 26 1993 Lightweight relevance filtering for machine-generated resolution problems. Zbl 1183.68560Meng, Jia; Paulson, Lawrence C. 26 2009 Source-level proof reconstruction for interactive theorem proving. Zbl 1144.68364Paulson, Lawrence C.; Susanto, Kong Woei 23 2007 Extending Sledgehammer with SMT solvers. Zbl 1314.68271Blanchette, Jasmin Christian; Böhme, Sascha; Paulson, Lawrence C. 23 2011 The Isabelle framework. Zbl 1165.68478Wenzel, Makarius; Paulson, Lawrence C.; Nipkow, Tobias 22 2008 Hammering towards QED. Zbl 1451.68318Blanchette, Jasmin C.; Kaliszyk, Cezary; Paulson, Lawrence C.; Urban, Josef 22 2016 A generic tableau prover and its integration with Isabelle. Zbl 0961.68116Paulson, Lawrence C. 22 1999 Natural deduction as higher-order resolution. Zbl 0613.68035Paulson, Lawrence C. 22 1986 Logic and computation. Interactive proof with Cambridge LCF. Zbl 0645.68041Paulson, Lawrence C. 21 1987 The higher-order prover Leo-II. Zbl 1356.68176Benzmüller, Christoph; Sultana, Nik; Paulson, Lawrence C.; Theiß, Frank 18 2015 Quantified multimodal logics in simple type theory. Zbl 1334.03014Benzmüller, Christoph; Paulson, Lawrence C. 15 2013 Multimodal and intuitionistic logics in simple type theory. Zbl 1222.03023Benzmüller, Christoph; Paulson, Lawrence C. 13 2010 Automation for interactive proof: first prototype. Zbl 1103.68113Meng, Jia; Quigley, Claire; Paulson, Lawrence C. 13 2006 Set theory for verification. II: Induction and recursion. Zbl 0840.68104Paulson, Lawrence C. 13 1995 A higher-order implementation of rewriting. Zbl 0551.68076Paulson, Lawrence 12 1983 Applying machine learning to the problem of choosing a heuristic to select the variable ordering for cylindrical algebraic decomposition. Zbl 1304.68224Huang, Zongyan; England, Matthew; Wilson, David; Davenport, James H.; Paulson, Lawrence C.; Bridge, James 10 2014 A machine-assisted proof of Gödel’s incompleteness theorems for the theory of hereditarily finite sets. Zbl 1337.03021Paulson, Lawrence C. 10 2014 Mechanizing coinduction and corecursion in higher-order logic. Zbl 0878.68111Paulson, Lawrence C. 9 1997 MetiTarski: past and future. Zbl 1360.68765Paulson, Lawrence C. 9 2012 Proof pearl: Defining functions over finite sets. Zbl 1152.68529Nipkow, Tobias; Paulson, Lawrence C. 9 2005 Machine learning for first-order theorem proving. Learning to select good heuristic. Zbl 1314.68274Bridge, James P.; Holden, Sean B.; Paulson, Lawrence C. 9 2014 Mechanizing set theory. Cardinal arithmetic and the axiom of choice. Zbl 0868.03005Paulson, Lawrence C.; Grąbczewski, Krzysztof 9 1996 Constructing recursion operators in intuitionistic type theory. Zbl 0631.03045Paulson, Lawrence C. 9 1986 Using machine learning to improve cylindrical algebraic decomposition. Zbl 1474.68464Huang, Zongyan; England, Matthew; Wilson, David J.; Bridge, James; Davenport, James H.; Paulson, Lawrence C. 8 2019 A mechanised proof of Gödel’s incompleteness theorems using Nominal Isabelle. Zbl 1357.68200Paulson, Lawrence C. 8 2015 Experiments on supporting interactive proof using resolution. Zbl 1126.68574Meng, Jia; Paulson, Lawrence C. 8 2004 Defining functions on equivalence classes. Zbl 1367.68254Paulson, Lawrence C. 8 2006 LEO-II and Satallax on the Sledgehammer test bench. Zbl 1262.68161Sultana, Nik; Blanchette, Jasmin Christian; Paulson, Lawrence C. 8 2013 The relative consistency of the axiom of choice mechanized using Isabelle/ZF. Zbl 1053.03009Paulson, Lawrence C. 7 2003 Exploring properties of normal multimodal logics in simple type theory with Leo-II. Zbl 1227.03017Benzmüller, Christoph; Paulson, Lawrence C. 7 2008 Verifying the unification algorithm in LCF. Zbl 0567.68054Paulson, Lawrence C. 6 1985 Proving termination of normalization functions for conditional expressions. Zbl 0642.68159Paulson, Lawrence C. 6 1986 Extending a resolution prover for inequalities on elementary functions. Zbl 1137.68571Akbarpour, Behzad; Paulson, Lawrence C. 6 2007 A formalisation of finite automata using hereditarily finite sets. Zbl 1465.68165Paulson, Lawrence C. 6 2015 From LCF to Isabelle/HOL. Zbl 1427.68349Paulson, Lawrence C.; Nipkow, Tobias; Wenzel, Makarius 5 2019 Mechanizing UNITY in Isabelle. Zbl 1365.68379Paulson, Lawrence C. 5 2000 A combination of nonstandard analysis and geometry theorem proving, with application to Newton’s Principia. Zbl 0924.03022Fleuriot, Jacques D.; Paulson, Lawrence C. 4 1998 A formal proof of Sylow’s theorem. An experiment in abstract algebra with Isabelle H0L. Zbl 0943.68149Kammüller, Florian; Paulson, Lawrence C. 4 1999 Organizing numerical theories using axiomatic type classes. Zbl 1071.68092Paulson, Lawrence C. 4 2004 Computational logic: its origins and applications. Zbl 1402.68160Paulson, Lawrence C. 3 2018 A fixedpoint approach to implementing (co)inductive definitions. Zbl 1433.68560Paulson, Lawrence C. 3 1994 An Isabelle/HOL formalisation of Green’s theorem. Zbl 1468.68312Abdulaziz, Mohammad; Paulson, Lawrence C. 3 2016 Verifying the SET purchase protocols. Zbl 1104.68465Bella, Giampaolo; Massacci, Fabio; Paulson, Lawrence C. 3 2006 MetiTarski: An automatic prover for the elementary functions. Zbl 1166.68335Akbarpour, Behzad; Paulson, Lawrence C. 3 2008 A pragmatic approach to extending provers by computer algebra – with applications to coding theory. Zbl 0951.68196Ballarin, Clemens; Paulson, Lawrence C. 3 1999 Proving Newton’s Propositio Kepleriana using geometry and nonstandard analysis in Isabelle. Zbl 0952.03004Fleuriot, Jacques D.; Paulson, Lawrence C. 2 1999 Deciding univariate polynomial problems using untrusted certificates in Isabelle/HOL. Zbl 1468.68298Li, Wenda; Passmore, Grant Olney; Paulson, Lawrence C. 2 2019 A formal proof of Cauchy’s residue theorem. Zbl 1478.68440Li, Wenda; Paulson, Lawrence C. 2 2016 Deriving structural induction in LCF. Zbl 0542.68075Paulson, Lawrence 2 1984 Lessons learned form LCF: A survey of natural deduction proofs. Zbl 0576.68070Paulson, Lawrence C. 2 1985 ML for the working programmer. Paperback ed. with corr. Zbl 0829.68013Paulson, Lawrence C. 2 1992 Applications of MetiTarski in the verification of control and hybrid systems. Zbl 1237.93087Akbarpour, Behzad; Paulson, Lawrence C. 2 2009 The reflection theorem: A study in meta-theoretic reasoning. Zbl 1072.68586Paulson, Lawrence C. 2 2002 Mechanizing nonstandard real analysis. Zbl 0951.03006Fleuriot, Jacques D.; Paulson, Lawrence C. 2 2000 Final coalgebras as greatest fixed points in ZF set theory. Zbl 0937.68047Paulson, Lawrence C. 2 1999 Real algebraic strategies for MetiTarski proofs. Zbl 1360.68764Passmore, Grant Olney; Paulson, Lawrence C.; de Moura, Leonardo 1 2012 Formalizing ordinal partition relations using Isabelle/HOL. Zbl 07566889Džamonja, Mirna; Koutsoukou-Argyraki, Angeliki; Paulson, Lawrence C. 1 2022 The relative consistency of the axiom of choice – mechanized using Isabelle/ZF. Zbl 1142.03332Paulson, Lawrence C. 1 2008 Mechanical proofs about a non-repudiation protocol. Zbl 1005.68538Bella, Giampaolo; Paulson, Lawrence C. 1 2001 An Isabelle/HOL formalisation of Green’s theorem. Zbl 1468.68313Abdulaziz, Mohammad; Paulson, Lawrence C. 1 2019 A formulation of the simple theory of types (for Isabelle). Zbl 0781.03007Paulson, Lawrence C. 1 1990 Interactive theorem proving. First international conference, ITP 2010, Edinburgh, UK, July 11–14, 2010. Proceedings. Zbl 1195.68009 1 2010 Evaluating winding numbers and counting complex roots through Cauchy indices in Isabelle/HOL. Zbl 1468.68299Li, Wenda; Paulson, Lawrence C. 1 2020 Formalizing ordinal partition relations using Isabelle/HOL. Zbl 07566889Džamonja, Mirna; Koutsoukou-Argyraki, Angeliki; Paulson, Lawrence C. 1 2022 Evaluating winding numbers and counting complex roots through Cauchy indices in Isabelle/HOL. Zbl 1468.68299Li, Wenda; Paulson, Lawrence C. 1 2020 Using machine learning to improve cylindrical algebraic decomposition. Zbl 1474.68464Huang, Zongyan; England, Matthew; Wilson, David J.; Bridge, James; Davenport, James H.; Paulson, Lawrence C. 8 2019 From LCF to Isabelle/HOL. Zbl 1427.68349Paulson, Lawrence C.; Nipkow, Tobias; Wenzel, Makarius 5 2019 Deciding univariate polynomial problems using untrusted certificates in Isabelle/HOL. Zbl 1468.68298Li, Wenda; Passmore, Grant Olney; Paulson, Lawrence C. 2 2019 An Isabelle/HOL formalisation of Green’s theorem. Zbl 1468.68313Abdulaziz, Mohammad; Paulson, Lawrence C. 1 2019 Computational logic: its origins and applications. Zbl 1402.68160Paulson, Lawrence C. 3 2018 Hammering towards QED. Zbl 1451.68318Blanchette, Jasmin C.; Kaliszyk, Cezary; Paulson, Lawrence C.; Urban, Josef 22 2016 An Isabelle/HOL formalisation of Green’s theorem. Zbl 1468.68312Abdulaziz, Mohammad; Paulson, Lawrence C. 3 2016 A formal proof of Cauchy’s residue theorem. Zbl 1478.68440Li, Wenda; Paulson, Lawrence C. 2 2016 The higher-order prover Leo-II. Zbl 1356.68176Benzmüller, Christoph; Sultana, Nik; Paulson, Lawrence C.; Theiß, Frank 18 2015 A mechanised proof of Gödel’s incompleteness theorems using Nominal Isabelle. Zbl 1357.68200Paulson, Lawrence C. 8 2015 A formalisation of finite automata using hereditarily finite sets. Zbl 1465.68165Paulson, Lawrence C. 6 2015 Applying machine learning to the problem of choosing a heuristic to select the variable ordering for cylindrical algebraic decomposition. Zbl 1304.68224Huang, Zongyan; England, Matthew; Wilson, David; Davenport, James H.; Paulson, Lawrence C.; Bridge, James 10 2014 A machine-assisted proof of Gödel’s incompleteness theorems for the theory of hereditarily finite sets. Zbl 1337.03021Paulson, Lawrence C. 10 2014 Machine learning for first-order theorem proving. Learning to select good heuristic. Zbl 1314.68274Bridge, James P.; Holden, Sean B.; Paulson, Lawrence C. 9 2014 Extending Sledgehammer with SMT solvers. Zbl 1314.68272Blanchette, Jasmin Christian; Böhme, Sascha; Paulson, Lawrence C. 36 2013 Quantified multimodal logics in simple type theory. Zbl 1334.03014Benzmüller, Christoph; Paulson, Lawrence C. 15 2013 LEO-II and Satallax on the Sledgehammer test bench. Zbl 1262.68161Sultana, Nik; Blanchette, Jasmin Christian; Paulson, Lawrence C. 8 2013 MetiTarski: past and future. Zbl 1360.68765Paulson, Lawrence C. 9 2012 Real algebraic strategies for MetiTarski proofs. Zbl 1360.68764Passmore, Grant Olney; Paulson, Lawrence C.; de Moura, Leonardo 1 2012 Extending Sledgehammer with SMT solvers. Zbl 1314.68271Blanchette, Jasmin Christian; Böhme, Sascha; Paulson, Lawrence C. 23 2011 MetiTarski: An automatic theorem prover for real-valued special functions. Zbl 1215.68206Akbarpour, Behzad; Paulson, Lawrence Charles 32 2010 Multimodal and intuitionistic logics in simple type theory. Zbl 1222.03023Benzmüller, Christoph; Paulson, Lawrence C. 13 2010 Interactive theorem proving. First international conference, ITP 2010, Edinburgh, UK, July 11–14, 2010. Proceedings. Zbl 1195.68009 1 2010 Lightweight relevance filtering for machine-generated resolution problems. Zbl 1183.68560Meng, Jia; Paulson, Lawrence C. 26 2009 Applications of MetiTarski in the verification of control and hybrid systems. Zbl 1237.93087Akbarpour, Behzad; Paulson, Lawrence C. 2 2009 Translating higher-order clauses to first-order clauses. Zbl 1203.68188Meng, Jia; Paulson, Lawrence C. 34 2008 LEO-II – a cooperative automatic theorem prover for classical higher-order logic. (System description). Zbl 1165.68446Benzmüller, Christoph; Paulson, Lawrence C.; Theiss, Frank; Fietzke, Arnaud 27 2008 The Isabelle framework. Zbl 1165.68478Wenzel, Makarius; Paulson, Lawrence C.; Nipkow, Tobias 22 2008 Exploring properties of normal multimodal logics in simple type theory with Leo-II. Zbl 1227.03017Benzmüller, Christoph; Paulson, Lawrence C. 7 2008 MetiTarski: An automatic prover for the elementary functions. Zbl 1166.68335Akbarpour, Behzad; Paulson, Lawrence C. 3 2008 The relative consistency of the axiom of choice – mechanized using Isabelle/ZF. Zbl 1142.03332Paulson, Lawrence C. 1 2008 Source-level proof reconstruction for interactive theorem proving. Zbl 1144.68364Paulson, Lawrence C.; Susanto, Kong Woei 23 2007 Extending a resolution prover for inequalities on elementary functions. Zbl 1137.68571Akbarpour, Behzad; Paulson, Lawrence C. 6 2007 Automation for interactive proof: first prototype. Zbl 1103.68113Meng, Jia; Quigley, Claire; Paulson, Lawrence C. 13 2006 Defining functions on equivalence classes. Zbl 1367.68254Paulson, Lawrence C. 8 2006 Verifying the SET purchase protocols. Zbl 1104.68465Bella, Giampaolo; Massacci, Fabio; Paulson, Lawrence C. 3 2006 Proof pearl: Defining functions over finite sets. Zbl 1152.68529Nipkow, Tobias; Paulson, Lawrence C. 9 2005 Experiments on supporting interactive proof using resolution. Zbl 1126.68574Meng, Jia; Paulson, Lawrence C. 8 2004 Organizing numerical theories using axiomatic type classes. Zbl 1071.68092Paulson, Lawrence C. 4 2004 The relative consistency of the axiom of choice mechanized using Isabelle/ZF. Zbl 1053.03009Paulson, Lawrence C. 7 2003 Isabelle/HOL. A proof assistant for higher-order logic. Zbl 0994.68131Nipkow, Tobias; Paulson, Lawrence C.; Wenzel, Markus 396 2002 The reflection theorem: A study in meta-theoretic reasoning. Zbl 1072.68586Paulson, Lawrence C. 2 2002 Mechanical proofs about a non-repudiation protocol. Zbl 1005.68538Bella, Giampaolo; Paulson, Lawrence C. 1 2001 Mechanizing UNITY in Isabelle. Zbl 1365.68379Paulson, Lawrence C. 5 2000 Mechanizing nonstandard real analysis. Zbl 0951.03006Fleuriot, Jacques D.; Paulson, Lawrence C. 2 2000 A generic tableau prover and its integration with Isabelle. Zbl 0961.68116Paulson, Lawrence C. 22 1999 A formal proof of Sylow’s theorem. An experiment in abstract algebra with Isabelle H0L. Zbl 0943.68149Kammüller, Florian; Paulson, Lawrence C. 4 1999 A pragmatic approach to extending provers by computer algebra – with applications to coding theory. Zbl 0951.68196Ballarin, Clemens; Paulson, Lawrence C. 3 1999 Proving Newton’s Propositio Kepleriana using geometry and nonstandard analysis in Isabelle. Zbl 0952.03004Fleuriot, Jacques D.; Paulson, Lawrence C. 2 1999 Final coalgebras as greatest fixed points in ZF set theory. Zbl 0937.68047Paulson, Lawrence C. 2 1999 A combination of nonstandard analysis and geometry theorem proving, with application to Newton’s Principia. Zbl 0924.03022Fleuriot, Jacques D.; Paulson, Lawrence C. 4 1998 Mechanizing coinduction and corecursion in higher-order logic. Zbl 0878.68111Paulson, Lawrence C. 9 1997 ML for the working programmer. 2nd ed. Zbl 0863.68032Paulson, L. C. 43 1996 Mechanizing set theory. Cardinal arithmetic and the axiom of choice. Zbl 0868.03005Paulson, Lawrence C.; Grąbczewski, Krzysztof 9 1996 Set theory for verification. II: Induction and recursion. Zbl 0840.68104Paulson, Lawrence C. 13 1995 Isabelle. A generic theorem prover. Zbl 0825.68059Paulson, Lawrence C. 106 1994 A fixedpoint approach to implementing (co)inductive definitions. Zbl 1433.68560Paulson, Lawrence C. 3 1994 Set theory for verification. I: From foundations to functions. Zbl 0802.68128Paulson, Lawrence C. 26 1993 ML for the working programmer. Paperback ed. with corr. Zbl 0829.68013Paulson, Lawrence C. 2 1992 A formulation of the simple theory of types (for Isabelle). Zbl 0781.03007Paulson, Lawrence C. 1 1990 The foundation of a generic theorem prover. Zbl 0679.68173Paulson, Lawrence C. 51 1989 Logic and computation. Interactive proof with Cambridge LCF. Zbl 0645.68041Paulson, Lawrence C. 21 1987 Natural deduction as higher-order resolution. Zbl 0613.68035Paulson, Lawrence C. 22 1986 Constructing recursion operators in intuitionistic type theory. Zbl 0631.03045Paulson, Lawrence C. 9 1986 Proving termination of normalization functions for conditional expressions. Zbl 0642.68159Paulson, Lawrence C. 6 1986 Verifying the unification algorithm in LCF. Zbl 0567.68054Paulson, Lawrence C. 6 1985 Lessons learned form LCF: A survey of natural deduction proofs. Zbl 0576.68070Paulson, Lawrence C. 2 1985 Deriving structural induction in LCF. Zbl 0542.68075Paulson, Lawrence 2 1984 A higher-order implementation of rewriting. Zbl 0551.68076Paulson, Lawrence 12 1983 all cited Publications top 5 cited Publications all top 5 Cited by 1,131 Authors 38 Paulson, Lawrence Charles 29 Blanchette, Jasmin Christian 28 Nipkow, Tobias 26 Benzmüller, Christoph Ewald 23 Urban, Josef 21 Kaliszyk, Cezary 17 Rabe, Florian 14 England, Matthew 11 Brown, Chad Edward 11 Davenport, James Harold 11 Guttmann, Walter 11 Popescu, Andrei 11 Thiemann, René 10 Hasan, Osman 10 Kohlhase, Michael 10 Traytel, Dmitry 9 Böhme, Sascha 9 Lochbihler, Andreas 9 Reynolds, Andrew 8 Basin, David A. 8 Bentkamp, Alexander 8 Fleuriot, Jacques D. 8 Lammich, Peter 8 Miller, Dale Allen 8 Struth, Georg 8 Tahar, Sofiène 8 Wolff, Burkhart 7 Cavalcanti, Ana 7 Foster, Simon 7 Sternagel, Christian 7 Tinelli, Cesare 7 Tourret, Sophie 7 Vukmirović, Petar 7 Waldmann, Uwe 7 Wenzel, Makarius 7 Woodcock, James C. P. 6 Avigad, Jeremy 6 Bundy, Alan 6 Fleury, Mathias 6 Horozal, Fulya 6 Mossakowski, Till 6 Nadathur, Gopalan 6 Preoteasa, Viorel 6 Sutcliffe, Geoff 6 Weber, Tjark 6 Yamada, Akihisa 6 Zeyda, Frank 5 Abdulaziz, Mohammad 5 Aransay, Jesús 5 Ballarin, Clemens 5 Barrett, Clark W. 5 Bradford, Russell J. 5 Cruanes, Simon 5 Divasón, Jose 5 Gauthier, Thibault 5 Jakubův, Jan 5 Klein, Gerwin 5 Marić, Filip 5 Norrish, Michael 5 Obua, Steven 5 Rizkallah, Christine 5 Schlichtkrull, Anders 5 Tarlecki, Andrzej 5 Wilson, David J. 4 Berghammer, Rudolf 4 Bertot, Yves 4 Dixon, Lucas 4 Farmer, William M. 4 Felty, Amy P. 4 Fuenmayor, David 4 Giesl, Jürgen 4 Giunchiglia, Fausto 4 Grov, Gudmund 4 Höfner, Peter 4 Immler, Fabian 4 Janičić, Predrag 4 Krauss, Alexander 4 Kremer, Gereon 4 Kühlwein, Daniel 4 Kunčar, Ondřej 4 Li, Wenda 4 Li, Yongjian 4 Meseguer Guaita, José 4 Middeldorp, Aart 4 Möller, Bernhard 4 Moore, J Strother 4 Narboux, Julien 4 Parrow, Joachim 4 Platzer, André 4 Smolka, Gert 4 Steen, Alexander 4 Théry, Laurent 4 Weidenbach, Christoph 4 Woltzenlogel Paleo, Bruno 3 Ábrahám, Erika 3 Amjad, Hasan 3 Armando, Alessandro 3 Avron, Arnon 3 Back, Ralph-Johan 3 Barbosa, Haniel ...and 1,031 more Authors all top 5 Cited in 72 Serials 167 Journal of Automated Reasoning 38 Theoretical Computer Science 38 Formal Aspects of Computing 29 Journal of Symbolic Computation 21 Journal of Logical and Algebraic Methods in Programming 18 Annals of Mathematics and Artificial Intelligence 17 Journal of Applied Logic 13 Formal Methods in System Design 11 Journal of Functional Programming 11 Logical Methods in Computer Science 9 Information and Computation 9 Mathematics in Computer Science 8 MSCS. Mathematical Structures in Computer Science 7 ACM Transactions on Computational Logic 6 The Journal of Logic and Algebraic Programming 5 Science of Computer Programming 5 Logica Universalis 4 Artificial Intelligence 4 Annals of Pure and Applied Logic 4 AI Communications 4 The Review of Symbolic Logic 3 Journal of Computer Science and Technology 3 Experimental Mathematics 3 Journal of Applied Non-Classical Logics 3 Higher-Order and Symbolic Computation 3 LMS Journal of Computation and Mathematics 3 Concurrency and Computation: Practice & Experience 3 Sādhanā 3 Journal of Formalized Reasoning 2 Acta Informatica 2 BIT 2 Synthese 2 Advances in Applied Clifford Algebras 2 The Bulletin of Symbolic Logic 2 Journal of Combinatorial Optimization 2 Fundamenta Informaticae 2 Theory and Practice of Logic Programming 1 Information Processing Letters 1 Jahresbericht der Deutschen Mathematiker-Vereinigung (DMV) 1 Mathematical Notes 1 The Mathematical Intelligencer 1 Cahiers de Topologie et Géométrie Différentielle Catégoriques 1 Journal of Economic Theory 1 Journal of Philosophical Logic 1 The Journal of Symbolic Logic 1 Studia Logica 1 Bulletin of the Section of Logic 1 New Generation Computing 1 Discrete & Computational Geometry 1 Journal of the American Mathematical Society 1 SIAM Journal on Discrete Mathematics 1 Journal of Cryptology 1 International Journal of Foundations of Computer Science 1 Communications in Statistics. Simulation and Computation 1 International Journal of Computer Mathematics 1 Pattern Recognition 1 Distributed Computing 1 Indagationes Mathematicae. New Series 1 Reliable Computing 1 INFORMS Journal on Computing 1 Mathematical Problems in Engineering 1 Soft Computing 1 Wuhan University Journal of Natural Sciences (WUJNS) 1 Journal of Applied Mathematics 1 Computer Languages, Systems & Structures 1 Electronic Notes in Theoretical Computer Science 1 Frontiers of Computer Science 1 Forum of Mathematics, Pi 1 Nonlinear Analysis. Theory, Methods & Applications 1 Philosophical Transactions A. Royal Society of London 1 Proceedings of the Royal Society of London. A. Mathematical, Physical and Engineering Sciences 1 Philosophical Transactions of the Royal Society of London. A. Mathematical, Physical and Engineering Sciences all top 5 Cited in 38 Fields 754 Computer science (68-XX) 269 Mathematical logic and foundations (03-XX) 16 Information and communication theory, circuits (94-XX) 14 Numerical analysis (65-XX) 13 Combinatorics (05-XX) 11 Category theory; homological algebra (18-XX) 9 Algebraic geometry (14-XX) 8 Commutative algebra (13-XX) 7 History and biography (01-XX) 7 Order, lattices, ordered algebraic structures (06-XX) 7 Operations research, mathematical programming (90-XX) 6 General and overarching topics; collections (00-XX) 6 Number theory (11-XX) 6 Real functions (26-XX) 6 Game theory, economics, finance, and other social and behavioral sciences (91-XX) 6 Systems theory; control (93-XX) 5 General algebraic systems (08-XX) 5 Linear and multilinear algebra; matrix theory (15-XX) 5 Geometry (51-XX) 5 Convex and discrete geometry (52-XX) 5 Probability theory and stochastic processes (60-XX) 4 Ordinary differential equations (34-XX) 3 Dynamical systems and ergodic theory (37-XX) 2 Field theory and polynomials (12-XX) 2 Group theory and generalizations (20-XX) 2 Several complex variables and analytic spaces (32-XX) 2 Special functions (33-XX) 2 Mechanics of particles and systems (70-XX) 2 Mathematics education (97-XX) 1 Functions of a complex variable (30-XX) 1 Approximations and expansions (41-XX) 1 Harmonic analysis on Euclidean spaces (42-XX) 1 General topology (54-XX) 1 Algebraic topology (55-XX) 1 Statistics (62-XX) 1 Fluid mechanics (76-XX) 1 Quantum theory (81-XX) 1 Biology and other natural sciences (92-XX) Citations by Year Wikidata Timeline The data are displayed as stored in Wikidata under a Creative Commons CC0 License. Updates and corrections should be made in Wikidata.