×

Paulson, Lawrence Charles

Author ID: paulson.lawrence-charles Recent zbMATH articles by "Paulson, Lawrence Charles"
Published as: Paulson, Lawrence C.; Paulson, Lawrence; Paulson, Lawrence Charles; Paulson, Larry; Paulson, L. C.
Homepage: https://www.cl.cam.ac.uk/~lp15/
External Links: MGP · ORCID · Wikidata · Google Scholar · dblp · IdRef · theses.fr

Publications by Year

Citations contained in zbMATH Open

81 Publications have been cited 1,535 times in 1,003 Documents Cited by Year
Isabelle/HOL. A proof assistant for higher-order logic. Zbl 0994.68131
Nipkow, Tobias; Paulson, Lawrence C.; Wenzel, Markus
494
2002
Isabelle. A generic theorem prover. Zbl 0825.68059
Paulson, Lawrence C.
132
1994
The foundation of a generic theorem prover. Zbl 0679.68173
Paulson, Lawrence C.
64
1989
ML for the working programmer. 2nd ed. Zbl 0863.68032
Paulson, L. C.
46
1996
Extending Sledgehammer with SMT solvers. Zbl 1314.68272
Blanchette, Jasmin Christian; Böhme, Sascha; Paulson, Lawrence C.
41
2013
Translating higher-order clauses to first-order clauses. Zbl 1203.68188
Meng, Jia; Paulson, Lawrence C.
37
2008
MetiTarski: An automatic theorem prover for real-valued special functions. Zbl 1215.68206
Akbarpour, Behzad; Paulson, Lawrence Charles
36
2010
Hammering towards QED. Zbl 1451.68318
Blanchette, Jasmin C.; Kaliszyk, Cezary; Paulson, Lawrence C.; Urban, Josef
35
2016
Set theory for verification. I: From foundations to functions. Zbl 0802.68128
Paulson, Lawrence C.
33
1993
Logic and computation. Interactive proof with Cambridge LCF. Zbl 0645.68041
Paulson, Lawrence C.
32
1987
LEO-II – a cooperative automatic theorem prover for classical higher-order logic. (System description). Zbl 1165.68446
Benzmüller, Christoph; Paulson, Lawrence C.; Theiss, Frank; Fietzke, Arnaud
31
2008
Natural deduction as higher-order resolution. Zbl 0613.68035
Paulson, Lawrence C.
29
1986
The Isabelle framework. Zbl 1165.68478
Wenzel, Makarius; Paulson, Lawrence C.; Nipkow, Tobias
28
2008
Lightweight relevance filtering for machine-generated resolution problems. Zbl 1183.68560
Meng, Jia; Paulson, Lawrence C.
28
2009
Extending Sledgehammer with SMT solvers. Zbl 1314.68271
Blanchette, Jasmin Christian; Böhme, Sascha; Paulson, Lawrence C.
27
2011
Source-level proof reconstruction for interactive theorem proving. Zbl 1144.68364
Paulson, Lawrence C.; Susanto, Kong Woei
25
2007
A generic tableau prover and its integration with Isabelle. Zbl 0961.68116
Paulson, Lawrence C.
22
1999
The higher-order prover Leo-II. Zbl 1356.68176
Benzmüller, Christoph; Sultana, Nik; Paulson, Lawrence C.; Theiß, Frank
21
2015
Quantified multimodal logics in simple type theory. Zbl 1334.03014
Benzmüller, Christoph; Paulson, Lawrence C.
18
2013
Set theory for verification. II: Induction and recursion. Zbl 0840.68104
Paulson, Lawrence C.
17
1995
Automation for interactive proof: first prototype. Zbl 1103.68113
Meng, Jia; Quigley, Claire; Paulson, Lawrence C.
15
2006
Applying machine learning to the problem of choosing a heuristic to select the variable ordering for cylindrical algebraic decomposition. Zbl 1304.68224
Huang, Zongyan; England, Matthew; Wilson, David; Davenport, James H.; Paulson, Lawrence C.; Bridge, James
15
2014
A mechanised proof of Gödel’s incompleteness theorems using Nominal Isabelle. Zbl 1357.68200
Paulson, Lawrence C.
14
2015
Multimodal and intuitionistic logics in simple type theory. Zbl 1222.03023
Benzmüller, Christoph; Paulson, Lawrence C.
13
2010
A higher-order implementation of rewriting. Zbl 0551.68076
Paulson, Lawrence
13
1983
Mechanizing set theory. Cardinal arithmetic and the axiom of choice. Zbl 0868.03005
Paulson, Lawrence C.; Grąbczewski, Krzysztof
12
1996
A fixedpoint approach to implementing (co)inductive definitions. Zbl 1433.68560
Paulson, Lawrence C.
12
1994
The relative consistency of the axiom of choice mechanized using Isabelle/ZF. Zbl 1053.03009
Paulson, Lawrence C.
11
2003
Mechanizing coinduction and corecursion in higher-order logic. Zbl 0878.68111
Paulson, Lawrence C.
11
1997
A machine-assisted proof of Gödel’s incompleteness theorems for the theory of hereditarily finite sets. Zbl 1337.03021
Paulson, Lawrence C.
11
2014
Constructing recursion operators in intuitionistic type theory. Zbl 0631.03045
Paulson, Lawrence C.
11
1986
MetiTarski: past and future. Zbl 1360.68765
Paulson, Lawrence C.
10
2012
Using machine learning to improve cylindrical algebraic decomposition. Zbl 1474.68464
Huang, Zongyan; England, Matthew; Wilson, David J.; Bridge, James; Davenport, James H.; Paulson, Lawrence C.
10
2019
Proof pearl: Defining functions over finite sets. Zbl 1152.68529
Nipkow, Tobias; Paulson, Lawrence C.
10
2005
Experiments on supporting interactive proof using resolution. Zbl 1126.68574
Meng, Jia; Paulson, Lawrence C.
9
2004
Machine learning for first-order theorem proving. Learning to select good heuristic. Zbl 1314.68274
Bridge, James P.; Holden, Sean B.; Paulson, Lawrence C.
9
2014
Defining functions on equivalence classes. Zbl 1367.68254
Paulson, Lawrence C.
9
2006
From LCF to Isabelle/HOL. Zbl 1427.68349
Paulson, Lawrence C.; Nipkow, Tobias; Wenzel, Makarius
9
2019
Exploring properties of normal multimodal logics in simple type theory with Leo-II. Zbl 1227.03017
Benzmüller, Christoph; Paulson, Lawrence C.
8
2008
Extending a resolution prover for inequalities on elementary functions. Zbl 1137.68571
Akbarpour, Behzad; Paulson, Lawrence C.
8
2007
LEO-II and Satallax on the Sledgehammer test bench. Zbl 1262.68161
Sultana, Nik; Blanchette, Jasmin Christian; Paulson, Lawrence C.
8
2013
Verifying the unification algorithm in LCF. Zbl 0567.68054
Paulson, Lawrence C.
7
1985
Mechanizing UNITY in Isabelle. Zbl 1365.68379
Paulson, Lawrence C.
6
2000
Proving termination of normalization functions for conditional expressions. Zbl 0642.68159
Paulson, Lawrence C.
6
1986
A formalisation of finite automata using hereditarily finite sets. Zbl 1465.68165
Paulson, Lawrence C.
6
2015
Formalizing ordinal partition relations using Isabelle/HOL. Zbl 1520.68217
Džamonja, Mirna; Koutsoukou-Argyraki, Angeliki; Paulson, Lawrence C.
6
2022
Computational logic: its origins and applications. Zbl 1402.68160
Paulson, Lawrence C.
5
2018
Organizing numerical theories using axiomatic type classes. Zbl 1071.68092
Paulson, Lawrence C.
5
2004
The reflection theorem: A study in meta-theoretic reasoning. Zbl 1072.68586
Paulson, Lawrence C.
5
2002
A pragmatic approach to extending provers by computer algebra – with applications to coding theory. Zbl 0951.68196
Ballarin, Clemens; Paulson, Lawrence C.
4
1999
A formal proof of Sylow’s theorem. An experiment in abstract algebra with Isabelle H0L. Zbl 0943.68149
Kammüller, Florian; Paulson, Lawrence C.
4
1999
A combination of nonstandard analysis and geometry theorem proving, with application to Newton’s Principia. Zbl 0924.03022
Fleuriot, Jacques D.; Paulson, Lawrence C.
4
1998
MetiTarski: An automatic prover for the elementary functions. Zbl 1166.68335
Akbarpour, Behzad; Paulson, Lawrence C.
4
2008
Verifying the SET purchase protocols. Zbl 1104.68465
Bella, Giampaolo; Massacci, Fabio; Paulson, Lawrence C.
3
2006
An Isabelle/HOL formalisation of Green’s theorem. Zbl 1468.68312
Abdulaziz, Mohammad; Paulson, Lawrence C.
3
2016
A modular first formalisation of combinatorial design theory. Zbl 1485.68291
Edmonds, Chelsea; Paulson, Lawrence C.
3
2021
Evaluating winding numbers and counting complex roots through Cauchy indices in Isabelle/HOL. Zbl 1468.68299
Li, Wenda; Paulson, Lawrence C.
3
2020
Final coalgebras as greatest fixed points in ZF set theory. Zbl 0937.68047
Paulson, Lawrence C.
2
1999
Proving Newton’s Propositio Kepleriana using geometry and nonstandard analysis in Isabelle. Zbl 0952.03004
Fleuriot, Jacques D.; Paulson, Lawrence C.
2
1999
Deciding univariate polynomial problems using untrusted certificates in Isabelle/HOL. Zbl 1468.68298
Li, Wenda; Passmore, Grant Olney; Paulson, Lawrence C.
2
2019
Mechanizing nonstandard real analysis. Zbl 0951.03006
Fleuriot, Jacques D.; Paulson, Lawrence C.
2
2000
Real algebraic strategies for MetiTarski proofs. Zbl 1360.68764
Passmore, Grant Olney; Paulson, Lawrence C.; de Moura, Leonardo
2
2012
ML for the working programmer. Paperback ed. with corr. Zbl 0829.68013
Paulson, Lawrence C.
2
1992
Applications of MetiTarski in the verification of control and hybrid systems. Zbl 1237.93087
Akbarpour, Behzad; Paulson, Lawrence C.
2
2009
A formal proof of Cauchy’s residue theorem. Zbl 1478.68440
Li, Wenda; Paulson, Lawrence C.
2
2016
Lessons learned form LCF: A survey of natural deduction proofs. Zbl 0576.68070
Paulson, Lawrence C.
2
1985
Deriving structural induction in LCF. Zbl 0542.68075
Paulson, Lawrence
2
1984
Simple type theory is not too simple: Grothendieck’s schemes without dependent types. Zbl 1498.14001
Bordg, Anthony; Paulson, Lawrence; Li, Wenda
2
2022
Algebraically closed fields in isabelle/HOL. Zbl 07614671
de Vilhena, Paulo Emílio; Paulson, Lawrence C.
2
2020
Wetzel: formalisation of an undecidable problem linked to the continuum hypothesis. Zbl 07691292
Paulson, Lawrence C.
2
2022
A formulation of the simple theory of types (for Isabelle). Zbl 0781.03007
Paulson, Lawrence C.
1
1990
Mechanical proofs about a non-repudiation protocol. Zbl 1005.68538
Bella, Giampaolo; Paulson, Lawrence C.
1
2001
A proof of non-repudiation. Zbl 1017.68574
Bella, Giampaolo; Paulson, Lawrence C.
1
2002
Interactive theorem proving. First international conference, ITP 2010, Edinburgh, UK, July 11–14, 2010. Proceedings. Zbl 1195.68009
1
2010
Introduction to “Milestones in interactive theorem proving”. Zbl 1398.00118
1
2018
An Isabelle/HOL formalisation of Green’s theorem. Zbl 1468.68313
Abdulaziz, Mohammad; Paulson, Lawrence C.
1
2019
The relative consistency of the axiom of choice – mechanized using Isabelle/ZF. Zbl 1142.03332
Paulson, Lawrence C.
1
2008
A formalised theorem in the partition calculus. Zbl 07748742
Paulson, Lawrence C.
1
2024
Irrationality and transcendence criteria for infinite series in Isabelle/HOL. Zbl 1518.11003
Koutsoukou-Argyraki, Angeliki; Li, Wenda; Paulson, Lawrence C.
1
2022
Logic programming, functional programming, and inductive definitions. Zbl 1502.68071
Paulson, Lawrence C.; Smith, Andrew W.
1
1991
Formalising Szemerédi’s Regularity Lemma and Roth’s Theorem on Arithmetic Progressions in Isabelle/HOL. Zbl 07695705
Edmonds, Chelsea; Koutsoukou-Argyraki, Angeliki; Paulson, Lawrence C.
1
2023
A formalised theorem in the partition calculus. Zbl 07748742
Paulson, Lawrence C.
1
2024
Formalising Szemerédi’s Regularity Lemma and Roth’s Theorem on Arithmetic Progressions in Isabelle/HOL. Zbl 07695705
Edmonds, Chelsea; Koutsoukou-Argyraki, Angeliki; Paulson, Lawrence C.
1
2023
Formalizing ordinal partition relations using Isabelle/HOL. Zbl 1520.68217
Džamonja, Mirna; Koutsoukou-Argyraki, Angeliki; Paulson, Lawrence C.
6
2022
Simple type theory is not too simple: Grothendieck’s schemes without dependent types. Zbl 1498.14001
Bordg, Anthony; Paulson, Lawrence; Li, Wenda
2
2022
Wetzel: formalisation of an undecidable problem linked to the continuum hypothesis. Zbl 07691292
Paulson, Lawrence C.
2
2022
Irrationality and transcendence criteria for infinite series in Isabelle/HOL. Zbl 1518.11003
Koutsoukou-Argyraki, Angeliki; Li, Wenda; Paulson, Lawrence C.
1
2022
A modular first formalisation of combinatorial design theory. Zbl 1485.68291
Edmonds, Chelsea; Paulson, Lawrence C.
3
2021
Evaluating winding numbers and counting complex roots through Cauchy indices in Isabelle/HOL. Zbl 1468.68299
Li, Wenda; Paulson, Lawrence C.
3
2020
Algebraically closed fields in isabelle/HOL. Zbl 07614671
de Vilhena, Paulo Emílio; Paulson, Lawrence C.
2
2020
Using machine learning to improve cylindrical algebraic decomposition. Zbl 1474.68464
Huang, Zongyan; England, Matthew; Wilson, David J.; Bridge, James; Davenport, James H.; Paulson, Lawrence C.
10
2019
From LCF to Isabelle/HOL. Zbl 1427.68349
Paulson, Lawrence C.; Nipkow, Tobias; Wenzel, Makarius
9
2019
Deciding univariate polynomial problems using untrusted certificates in Isabelle/HOL. Zbl 1468.68298
Li, Wenda; Passmore, Grant Olney; Paulson, Lawrence C.
2
2019
An Isabelle/HOL formalisation of Green’s theorem. Zbl 1468.68313
Abdulaziz, Mohammad; Paulson, Lawrence C.
1
2019
Computational logic: its origins and applications. Zbl 1402.68160
Paulson, Lawrence C.
5
2018
Introduction to “Milestones in interactive theorem proving”. Zbl 1398.00118
1
2018
Hammering towards QED. Zbl 1451.68318
Blanchette, Jasmin C.; Kaliszyk, Cezary; Paulson, Lawrence C.; Urban, Josef
35
2016
An Isabelle/HOL formalisation of Green’s theorem. Zbl 1468.68312
Abdulaziz, Mohammad; Paulson, Lawrence C.
3
2016
A formal proof of Cauchy’s residue theorem. Zbl 1478.68440
Li, Wenda; Paulson, Lawrence C.
2
2016
The higher-order prover Leo-II. Zbl 1356.68176
Benzmüller, Christoph; Sultana, Nik; Paulson, Lawrence C.; Theiß, Frank
21
2015
A mechanised proof of Gödel’s incompleteness theorems using Nominal Isabelle. Zbl 1357.68200
Paulson, Lawrence C.
14
2015
A formalisation of finite automata using hereditarily finite sets. Zbl 1465.68165
Paulson, 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.68224
Huang, Zongyan; England, Matthew; Wilson, David; Davenport, James H.; Paulson, Lawrence C.; Bridge, James
15
2014
A machine-assisted proof of Gödel’s incompleteness theorems for the theory of hereditarily finite sets. Zbl 1337.03021
Paulson, Lawrence C.
11
2014
Machine learning for first-order theorem proving. Learning to select good heuristic. Zbl 1314.68274
Bridge, James P.; Holden, Sean B.; Paulson, Lawrence C.
9
2014
Extending Sledgehammer with SMT solvers. Zbl 1314.68272
Blanchette, Jasmin Christian; Böhme, Sascha; Paulson, Lawrence C.
41
2013
Quantified multimodal logics in simple type theory. Zbl 1334.03014
Benzmüller, Christoph; Paulson, Lawrence C.
18
2013
LEO-II and Satallax on the Sledgehammer test bench. Zbl 1262.68161
Sultana, Nik; Blanchette, Jasmin Christian; Paulson, Lawrence C.
8
2013
MetiTarski: past and future. Zbl 1360.68765
Paulson, Lawrence C.
10
2012
Real algebraic strategies for MetiTarski proofs. Zbl 1360.68764
Passmore, Grant Olney; Paulson, Lawrence C.; de Moura, Leonardo
2
2012
Extending Sledgehammer with SMT solvers. Zbl 1314.68271
Blanchette, Jasmin Christian; Böhme, Sascha; Paulson, Lawrence C.
27
2011
MetiTarski: An automatic theorem prover for real-valued special functions. Zbl 1215.68206
Akbarpour, Behzad; Paulson, Lawrence Charles
36
2010
Multimodal and intuitionistic logics in simple type theory. Zbl 1222.03023
Benzmü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.68560
Meng, Jia; Paulson, Lawrence C.
28
2009
Applications of MetiTarski in the verification of control and hybrid systems. Zbl 1237.93087
Akbarpour, Behzad; Paulson, Lawrence C.
2
2009
Translating higher-order clauses to first-order clauses. Zbl 1203.68188
Meng, Jia; Paulson, Lawrence C.
37
2008
LEO-II – a cooperative automatic theorem prover for classical higher-order logic. (System description). Zbl 1165.68446
Benzmüller, Christoph; Paulson, Lawrence C.; Theiss, Frank; Fietzke, Arnaud
31
2008
The Isabelle framework. Zbl 1165.68478
Wenzel, Makarius; Paulson, Lawrence C.; Nipkow, Tobias
28
2008
Exploring properties of normal multimodal logics in simple type theory with Leo-II. Zbl 1227.03017
Benzmüller, Christoph; Paulson, Lawrence C.
8
2008
MetiTarski: An automatic prover for the elementary functions. Zbl 1166.68335
Akbarpour, Behzad; Paulson, Lawrence C.
4
2008
The relative consistency of the axiom of choice – mechanized using Isabelle/ZF. Zbl 1142.03332
Paulson, Lawrence C.
1
2008
Source-level proof reconstruction for interactive theorem proving. Zbl 1144.68364
Paulson, Lawrence C.; Susanto, Kong Woei
25
2007
Extending a resolution prover for inequalities on elementary functions. Zbl 1137.68571
Akbarpour, Behzad; Paulson, Lawrence C.
8
2007
Automation for interactive proof: first prototype. Zbl 1103.68113
Meng, Jia; Quigley, Claire; Paulson, Lawrence C.
15
2006
Defining functions on equivalence classes. Zbl 1367.68254
Paulson, Lawrence C.
9
2006
Verifying the SET purchase protocols. Zbl 1104.68465
Bella, Giampaolo; Massacci, Fabio; Paulson, Lawrence C.
3
2006
Proof pearl: Defining functions over finite sets. Zbl 1152.68529
Nipkow, Tobias; Paulson, Lawrence C.
10
2005
Experiments on supporting interactive proof using resolution. Zbl 1126.68574
Meng, Jia; Paulson, Lawrence C.
9
2004
Organizing numerical theories using axiomatic type classes. Zbl 1071.68092
Paulson, Lawrence C.
5
2004
The relative consistency of the axiom of choice mechanized using Isabelle/ZF. Zbl 1053.03009
Paulson, Lawrence C.
11
2003
Isabelle/HOL. A proof assistant for higher-order logic. Zbl 0994.68131
Nipkow, Tobias; Paulson, Lawrence C.; Wenzel, Markus
494
2002
The reflection theorem: A study in meta-theoretic reasoning. Zbl 1072.68586
Paulson, Lawrence C.
5
2002
A proof of non-repudiation. Zbl 1017.68574
Bella, Giampaolo; Paulson, Lawrence C.
1
2002
Mechanical proofs about a non-repudiation protocol. Zbl 1005.68538
Bella, Giampaolo; Paulson, Lawrence C.
1
2001
Mechanizing UNITY in Isabelle. Zbl 1365.68379
Paulson, Lawrence C.
6
2000
Mechanizing nonstandard real analysis. Zbl 0951.03006
Fleuriot, Jacques D.; Paulson, Lawrence C.
2
2000
A generic tableau prover and its integration with Isabelle. Zbl 0961.68116
Paulson, Lawrence C.
22
1999
A pragmatic approach to extending provers by computer algebra – with applications to coding theory. Zbl 0951.68196
Ballarin, Clemens; Paulson, Lawrence C.
4
1999
A formal proof of Sylow’s theorem. An experiment in abstract algebra with Isabelle H0L. Zbl 0943.68149
Kammüller, Florian; Paulson, Lawrence C.
4
1999
Final coalgebras as greatest fixed points in ZF set theory. Zbl 0937.68047
Paulson, Lawrence C.
2
1999
Proving Newton’s Propositio Kepleriana using geometry and nonstandard analysis in Isabelle. Zbl 0952.03004
Fleuriot, Jacques D.; Paulson, Lawrence C.
2
1999
A combination of nonstandard analysis and geometry theorem proving, with application to Newton’s Principia. Zbl 0924.03022
Fleuriot, Jacques D.; Paulson, Lawrence C.
4
1998
Mechanizing coinduction and corecursion in higher-order logic. Zbl 0878.68111
Paulson, Lawrence C.
11
1997
ML for the working programmer. 2nd ed. Zbl 0863.68032
Paulson, L. C.
46
1996
Mechanizing set theory. Cardinal arithmetic and the axiom of choice. Zbl 0868.03005
Paulson, Lawrence C.; Grąbczewski, Krzysztof
12
1996
Set theory for verification. II: Induction and recursion. Zbl 0840.68104
Paulson, Lawrence C.
17
1995
Isabelle. A generic theorem prover. Zbl 0825.68059
Paulson, Lawrence C.
132
1994
A fixedpoint approach to implementing (co)inductive definitions. Zbl 1433.68560
Paulson, Lawrence C.
12
1994
Set theory for verification. I: From foundations to functions. Zbl 0802.68128
Paulson, Lawrence C.
33
1993
ML for the working programmer. Paperback ed. with corr. Zbl 0829.68013
Paulson, Lawrence C.
2
1992
Logic programming, functional programming, and inductive definitions. Zbl 1502.68071
Paulson, Lawrence C.; Smith, Andrew W.
1
1991
A formulation of the simple theory of types (for Isabelle). Zbl 0781.03007
Paulson, Lawrence C.
1
1990
The foundation of a generic theorem prover. Zbl 0679.68173
Paulson, Lawrence C.
64
1989
Logic and computation. Interactive proof with Cambridge LCF. Zbl 0645.68041
Paulson, Lawrence C.
32
1987
Natural deduction as higher-order resolution. Zbl 0613.68035
Paulson, Lawrence C.
29
1986
Constructing recursion operators in intuitionistic type theory. Zbl 0631.03045
Paulson, Lawrence C.
11
1986
Proving termination of normalization functions for conditional expressions. Zbl 0642.68159
Paulson, Lawrence C.
6
1986
Verifying the unification algorithm in LCF. Zbl 0567.68054
Paulson, Lawrence C.
7
1985
Lessons learned form LCF: A survey of natural deduction proofs. Zbl 0576.68070
Paulson, Lawrence C.
2
1985
Deriving structural induction in LCF. Zbl 0542.68075
Paulson, Lawrence
2
1984
A higher-order implementation of rewriting. Zbl 0551.68076
Paulson, Lawrence
13
1983
all top 5

Cited by 1,360 Authors

48 Paulson, Lawrence Charles
34 Nipkow, Tobias
32 Blanchette, Jasmin Christian
29 Benzmüller, Christoph Ewald
26 Urban, Josef
24 Kaliszyk, Cezary
20 Rabe, Florian
15 England, Matthew
15 Popescu, Andrei
13 Guttmann, Walter
12 Kohlhase, Michael
12 Thiemann, René
11 Brown, Chad Edward
11 Davenport, James Harold
11 Hasan, Osman
11 Traytel, Dmitry
10 Basin, David A.
10 Bentkamp, Alexander
10 Fleuriot, Jacques D.
10 Lochbihler, Andreas
10 Miller, Dale Allen
10 Struth, Georg
10 Sutcliffe, Geoff
9 Böhme, Sascha
9 Foster, Simon
9 Reynolds, Andrew
9 Sternagel, Christian
9 Tahar, Sofiène
9 Vukmirović, Petar
9 Wenzel, Makarius
9 Woodcock, James C. P.
8 Cavalcanti, Ana
8 Lammich, Peter
8 Marić, Filip
8 Tourret, Sophie
8 Wolff, Burkhart
7 Aransay, Jesús
7 Bundy, Alan
7 Divasón, Jose
7 Kunčar, Ondřej
7 Preoteasa, Viorel
7 Tinelli, Cesare
7 Waldmann, Uwe
7 Zeyda, Frank
6 Avigad, Jeremy
6 Felty, Amy P.
6 Fleury, Mathias
6 Horozal, Fulya
6 Jakubův, Jan
6 Klein, Gerwin
6 Mossakowski, Till
6 Nadathur, Gopalan
6 Platzer, André
6 Schlichtkrull, Anders
6 Smolka, Gert
6 Steen, Alexander
6 Tarlecki, Andrzej
6 Vyskočil, Jiří
6 Weber, Tjark
6 Yamada, Akihisa
5 Abdulaziz, Mohammad
5 Ballarin, Clemens
5 Barrett, Clark W.
5 Bradford, Russell J.
5 Brucker, Achim D.
5 Cruanes, Simon
5 Farmer, William M.
5 Fuenmayor, David
5 Gauthier, Thibault
5 Immler, Fabian
5 Kumar, Ramana
5 Norrish, Michael
5 Obua, Steven
5 Pąk, Karol
5 Reif, Wolfgang
5 Rizkallah, Christine
5 Wilson, David J.
4 Akbarpour, Behzad
4 Berghammer, Rudolf
4 Bertot, Yves
4 de Boer, Frank S.
4 Dixon, Lucas
4 Dongol, Brijesh
4 Giesl, Jürgen
4 Giunchiglia, Fausto
4 Grov, Gudmund
4 Höfner, Peter
4 Janičić, Predrag
4 Johansson, Moa
4 Kirchner, Hélène
4 Koutsoukou-Argyraki, Angeliki
4 Krauss, Alexander
4 Kremer, Gereon
4 Kühlwein, Daniel
4 Kuncak, Viktor
4 Li, Wenda
4 Li, Yongjian
4 Meseguer Guaita, José
4 Middeldorp, Aart
4 Möller, Bernhard
...and 1,260 more Authors
all top 5

Cited in 80 Serials

180 Journal of Automated Reasoning
45 Theoretical Computer Science
44 Formal Aspects of Computing
37 Journal of Symbolic Computation
23 Journal of Logical and Algebraic Methods in Programming
19 Annals of Mathematics and Artificial Intelligence
17 Journal of Applied Logic
16 Formal Methods in System Design
14 Logical Methods in Computer Science
13 Information and Computation
12 Journal of Functional Programming
9 MSCS. Mathematical Structures in Computer Science
9 Mathematics in Computer Science
8 The Journal of Logic and Algebraic Programming
7 ACM Transactions on Computational Logic
6 Artificial Intelligence
6 Annals of Pure and Applied Logic
5 Science of Computer Programming
5 Logica Universalis
4 AI Communications
4 Theory and Practice of Logic Programming
4 The Review of Symbolic Logic
4 Journal of Formalized Reasoning
3 Acta Informatica
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ā
2 BIT
2 Information Sciences
2 Journal of Philosophical Logic
2 Synthese
2 Advances in Applied Clifford Algebras
2 The Bulletin of Symbolic Logic
2 Journal of Combinatorial Optimization
2 Fundamenta Informaticae
2 Computer Languages, Systems & Structures
1 International Journal of Theoretical Physics
1 Information Processing Letters
1 Jahresbericht der Deutschen Mathematiker-Vereinigung (DMV)
1 Journal of Mathematical Physics
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 The Journal of Symbolic Logic
1 Programming and Computer Software
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 Neural Networks
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 Electronic Notes in Theoretical Computer Science
1 Involve
1 Journal of Theoretical Biology
1 Frontiers of Computer Science
1 Forum of Mathematics, Pi
1 Computer Science Review
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 40 Fields

935 Computer science (68-XX)
337 Mathematical logic and foundations (03-XX)
20 Information and communication theory, circuits (94-XX)
17 Numerical analysis (65-XX)
16 Combinatorics (05-XX)
13 Category theory; homological algebra (18-XX)
12 Algebraic geometry (14-XX)
11 Commutative algebra (13-XX)
9 Linear and multilinear algebra; matrix theory (15-XX)
8 General and overarching topics; collections (00-XX)
8 Systems theory; control (93-XX)
7 History and biography (01-XX)
7 Order, lattices, ordered algebraic structures (06-XX)
7 Number theory (11-XX)
7 Real functions (26-XX)
7 Operations research, mathematical programming (90-XX)
7 Game theory, economics, finance, and other social and behavioral sciences (91-XX)
6 Ordinary differential equations (34-XX)
6 Geometry (51-XX)
5 General algebraic systems (08-XX)
5 Convex and discrete geometry (52-XX)
5 Probability theory and stochastic processes (60-XX)
4 Group theory and generalizations (20-XX)
4 Dynamical systems and ergodic theory (37-XX)
4 Quantum theory (81-XX)
4 Biology and other natural sciences (92-XX)
2 Field theory and polynomials (12-XX)
2 Several complex variables and analytic spaces (32-XX)
2 Special functions (33-XX)
2 Algebraic topology (55-XX)
2 Statistics (62-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 Fluid mechanics (76-XX)
1 Relativity and gravitational theory (83-XX)
1 Geophysics (86-XX)

Citations by Year

The data are displayed as stored in Wikidata under a Creative Commons CC0 License. Updates and corrections should be made in Wikidata.