Journal of Automated Reasoning Short Title: J. Autom. Reasoning Publisher: Springer Netherlands, Dordrecht ISSN: 0168-7433; 1573-0670/e Online: https://link.springer.com/journal/10817/volumes-and-issues Comments: Journal; Indexed cover-to-cover Documents Indexed: 1,154 Publications (since 1985) References Indexed: 813 Publications with 28,471 References. all top 5 Latest Issues 68, No. 1 (2024) 67, No. 4 (2023) 67, No. 3 (2023) 67, No. 2 (2023) 67, No. 1 (2023) 66, No. 4 (2022) 66, No. 3 (2022) 66, No. 2 (2022) 66, No. 1 (2022) 65, No. 8 (2021) 65, No. 7 (2021) 65, No. 6 (2021) 65, No. 5 (2021) 65, No. 4 (2021) 65, No. 3 (2021) 65, No. 2 (2021) 65, No. 1 (2021) 64, No. 8 (2020) 64, No. 7 (2020) 64, No. 6 (2020) 64, No. 5 (2020) 64, No. 4 (2020) 64, No. 3 (2020) 64, No. 2 (2020) 64, No. 1 (2020) 63, No. 4 (2019) 63, No. 3 (2019) 63, No. 2 (2019) 63, No. 1 (2019) 62, No. 4 (2019) 62, No. 3 (2019) 62, No. 2 (2019) 62, No. 1 (2019) 61, No. 1-4 (2018) 60, No. 4 (2018) 60, No. 3 (2018) 60, No. 2 (2018) 60, No. 1 (2018) 59, No. 4 (2017) 59, No. 3 (2017) 59, No. 2 (2017) 59, No. 1 (2017) 58, No. 4 (2017) 58, No. 3 (2017) 58, No. 2 (2017) 58, No. 1 (2017) 57, No. 4 (2016) 57, No. 3 (2016) 57, No. 2 (2016) 57, No. 1 (2016) 56, No. 4 (2016) 56, No. 3 (2016) 56, No. 2 (2016) 56, No. 1 (2016) 55, No. 4 (2015) 55, No. 3 (2015) 55, No. 2 (2015) 55, No. 1 (2015) 54, No. 4 (2015) 54, No. 3 (2015) 54, No. 2 (2015) 54, No. 1 (2015) 53, No. 4 (2014) 53, No. 3 (2014) 53, No. 2 (2014) 53, No. 1 (2014) 52, No. 4 (2014) 52, No. 3 (2014) 52, No. 2 (2014) 52, No. 1 (2014) 51, No. 4 (2013) 51, No. 3 (2013) 51, No. 2 (2013) 51, No. 1 (2013) 50, No. 4 (2013) 50, No. 3 (2013) 50, No. 2 (2013) 50, No. 1 (2013) 49, No. 4 (2012) 49, No. 3 (2012) 49, No. 2 (2012) 49, No. 1 (2012) 48, No. 4 (2012) 48, No. 3 (2012) 48, No. 2 (2012) 48, No. 1 (2012) 47, No. 4 (2011) 47, No. 3 (2011) 47, No. 2 (2011) 47, No. 1 (2011) 46, No. 3-4 (2011) 46, No. 2 (2011) 46, No. 1 (2011) 45, No. 4 (2010) 45, No. 3 (2010) 45, No. 2 (2010) 45, No. 1 (2010) 44, No. 4 (2010) 44, No. 3 (2010) 44, No. 1-2 (2010) ...and 125 more Volumes all top 5 Authors 38 Wos, Larry 20 Paulson, Lawrence Charles 18 Blanchette, Jasmin Christian 12 Bonacina, Maria Paola 12 Nipkow, Tobias 12 Peltier, Nicolas 12 Sutcliffe, Geoff 12 Urban, Josef 11 Bundy, Alan 11 Chou, Shangching 11 Giesl, Jürgen 11 McCune, William W. 10 Plaisted, David Alan 9 Gao, Xiaoshan 9 Kaliszyk, Cezary 9 Veroff, Robert 8 Barrett, Clark W. 8 Kapur, Deepak 8 Kaufmann, Matt 8 Leroy, Xavier 8 Moore, J Strother 8 Norrish, Michael 8 Thiemann, René 7 Cantone, Domenico 7 Echenim, Mnacho 7 Heule, Marijn J. H. 7 Hustadt, Ullrich 7 Lammich, Peter 7 Middeldorp, Aart 7 Popescu, Andrei 7 Schneider-Kamp, Peter 7 Tinelli, Cesare 7 Weidenbach, Christoph 6 Ayala-Rincón, Mauricio 6 Baumgartner, Peter 6 Blazy, Sandrine 6 Felty, Amy P. 6 Policriti, Alberto 6 Rusinowitch, Michaël 6 Schmidt, Renate A. 6 Stickel, Mark E. 6 Tourret, Sophie 6 Walsh, Toby 6 Yahya, Adnan H. 6 Zhang, Hantao 6 Zhang, Jingzhong 5 Appel, Andrew W. 5 Avigad, Jeremy 5 Baader, Franz 5 Basin, David A. 5 Biere, Armin 5 Cristiá, Maximiliano 5 de Moura, Leonardo 5 Divasón, Jose 5 Dixon, Clare 5 Fiorino, Guido 5 Ghilardi, Silvio 5 Hähnle, Reiner 5 Henschen, Lawrence J. 5 Horrocks, Ian 5 Janičić, Predrag 5 Kazakov, Yevgeny 5 Kunen, Kenneth 5 Lochbihler, Andreas 5 Lucas, Salvador 5 Melquiond, Guillaume 5 Miller, Dale Allen 5 Muñoz, César A. 5 Narboux, Julien 5 Narendran, Paliath 5 Ohlbach, Hans Jürgen 5 Pąk, Karol 5 Reynolds, Andrew 5 Smolka, Gert 5 Subrahmanian, V. S. 5 Urban, Christian 5 Waldmann, Uwe 5 Yamada, Akihisa 4 Andrews, Peter B. 4 Barthe, Gilles 4 Bentkamp, Alexander 4 Beyersdorff, Olaf 4 Bledsoe, Woodrow W. 4 Böhme, Sascha 4 Calvanese, Diego 4 Cialdea Mayer, Marta 4 Delaune, Stéphanie 4 Fitelson, Branden 4 Fontaine, Pascal 4 Gamboa, Ruben A. 4 Giunchiglia, Fausto 4 Klein, Gerwin 4 Kohlhase, Michael 4 Korniłowicz, Artur 4 Kremer, Steve 4 Kröning, Daniel 4 Loveland, Donald W. 4 Lu, James J. 4 Lusk, Ewing L. 4 Maggesi, Marco ...and 1,470 more Authors all top 5 Fields 1,073 Computer science (68-XX) 448 Mathematical logic and foundations (03-XX) 39 General and overarching topics; collections (00-XX) 30 Information and communication theory, circuits (94-XX) 19 Group theory and generalizations (20-XX) 18 Number theory (11-XX) 17 Geometry (51-XX) 15 Operations research, mathematical programming (90-XX) 13 Numerical analysis (65-XX) 10 Order, lattices, ordered algebraic structures (06-XX) 10 Commutative algebra (13-XX) 9 History and biography (01-XX) 9 Combinatorics (05-XX) 9 Category theory; homological algebra (18-XX) 6 Algebraic topology (55-XX) 4 Field theory and polynomials (12-XX) 4 Linear and multilinear algebra; matrix theory (15-XX) 4 Game theory, economics, finance, and other social and behavioral sciences (91-XX) 3 Algebraic geometry (14-XX) 3 Nonassociative rings and algebras (17-XX) 3 Real functions (26-XX) 3 Ordinary differential equations (34-XX) 3 Convex and discrete geometry (52-XX) 3 Differential geometry (53-XX) 3 Probability theory and stochastic processes (60-XX) 3 Quantum theory (81-XX) 3 Relativity and gravitational theory (83-XX) 3 Systems theory; control (93-XX) 2 Associative rings and algebras (16-XX) 2 Functions of a complex variable (30-XX) 2 Several complex variables and analytic spaces (32-XX) 2 Special functions (33-XX) 2 Dynamical systems and ergodic theory (37-XX) 2 General topology (54-XX) 1 Measure and integration (28-XX) 1 Partial differential equations (35-XX) 1 Approximations and expansions (41-XX) 1 Mechanics of particles and systems (70-XX) 1 Biology and other natural sciences (92-XX) 1 Mathematics education (97-XX) Publications by Year all cited Publications top 5 cited Publications Citations contained in zbMATH Open 848 Publications have been cited 7,412 times in 4,252 Documents Cited by ▼ Year ▼ Tractable reasoning and efficient query answering in description logics: The DL-Lite family. Zbl 1132.68725 Calvanese, Diego; De Giacomo, Giuseppe; Lembo, Domenico; Lenzerini, Maurizio; Rosati, Riccardo 124 2007 The TPTP problem library and associated infrastructure and associated infrastructure. The FOF and CNF parts, v3.5.0. Zbl 1185.68636 Sutcliffe, Geoff 109 2009 The role of the Mizar mathematical library for interactive proof development in Mizar. Zbl 1433.68530 Bancerek, Grzegorz; Byliński, Czesław; Grabowski, Adam; Korniłowicz, Artur; Matuszewski, Roman; Naumowicz, Adam; Pąk, Karol 94 2018 Basic principles of mechanical theorem proving in elementary geometries. Zbl 0642.68163 Wu, Wentsun 73 1986 Four decades of {Mizar}. Foreword. Zbl 1336.00111 73 2015 The TPTP problem library. CNF release v1. 2. 1. Zbl 0910.68197 Sutcliffe, Geoff; Suttner, Christian 69 1998 Theorem proving modulo. Zbl 1049.03011 Dowek, Gilles; Hardin, Thérèse; Kirchner, Claude 64 2003 The foundation of a generic theorem prover. Zbl 0679.68173 Paulson, Lawrence C. 63 1989 Mechanizing and improving dependency pairs. Zbl 1113.68088 Giesl, Jürgen; Thiemann, René; Schneider-Kamp, Peter; Falke, Stephan 62 2006 Nominal techniques in Isabelle/HOL. Zbl 1140.68061 Urban, Christian 59 2008 Algorithms for computing minimal unsatisfiable subsets of constraints. Zbl 1154.68510 Liffiton, Mark H.; Sakallah, Karem A. 58 2008 Heavy-tailed phenomena in satisfiability and constraint satisfaction problems. Zbl 0967.68145 Gomes, Carla P.; Selman, Bart; Crato, Nuno; Kautz, Henry 58 2000 Differential dynamic logic for hybrid systems. Zbl 1181.03035 Platzer, André 56 2008 Matrix interpretations for proving termination of term rewriting. Zbl 1139.68049 Endrullis, Jörg; Waldmann, Johannes; Zantema, Hans 52 2008 A Prolog technology theorem prover: Implementation by an extended Prolog compiler. Zbl 0662.68104 Stickel, Mark E. 51 1988 SETHEO: A high-performance theorem prover. Zbl 0759.68080 Letz, R.; Schumann, J.; Bayerl, S.; Bibel, W. 50 1992 The TPTP problem library and associated infrastructure. From CNF to TH0, TPTP v6.4.0. Zbl 1425.68381 Sutcliffe, Geoff 49 2017 Automated deduction by theory resolution. Zbl 0616.68076 Stickel, Mark E. 48 1985 Solution of the Robbins problem. Zbl 0883.06011 McCune, William 47 1997 MPTP 0.2: Design, implementation, and initial experiments. Zbl 1113.68095 Urban, Josef 45 2006 Answer set programming based on propositional satisfiability. Zbl 1107.68029 Giunchiglia, Enrico; Lierler, Yuliya; Maratea, Marco 44 2006 The HOL Light theory of Euclidean space. Zbl 1260.68373 Harrison, John 42 2013 A tableau decision procedure for \(\mathcal{SHOIQ}\). Zbl 1132.68734 Horrocks, Ian; Sattler, Ulrike 41 2007 Inferring from inconsistency in preference-based argumentation frameworks. Zbl 1056.68589 Amgoud, Leila; Cayrol, Claudette 41 2002 Extending Sledgehammer with SMT solvers. Zbl 1314.68272 Blanchette, Jasmin Christian; Böhme, Sascha; Paulson, Lawrence C. 41 2013 Seventy-five problems for testing automatic theorem provers. Zbl 0642.68147 Pelletier, Francis Jeffry 39 1986 Automatic discovery of theorems in elementary geometry. Zbl 0941.03010 Recio, T.; Vélez, M. P. 38 1999 Locales: a module system for mathematical theories. Zbl 1315.68218 Ballarin, Clemens 38 2014 Translating higher-order clauses to first-order clauses. Zbl 1203.68188 Meng, Jia; Paulson, Lawrence C. 37 2008 Learning-assisted automated reasoning with \(\mathsf{Flyspeck}\). Zbl 1314.68283 Kaliszyk, Cezary; Urban, Josef 36 2014 Premise selection for mathematics by corpus analysis and kernel methods. Zbl 1315.68217 Alama, Jesse; Heskes, Tom; Kühlwein, Daniel; Tsivtsivadze, Evgeni; Urban, Josef 36 2014 MetiTarski: An automatic theorem prover for real-valued special functions. Zbl 1215.68206 Akbarpour, Behzad; Paulson, Lawrence Charles 35 2010 Controlled integration of the cut rule into connection tableau calculi. Zbl 0816.03005 Letz, R.; Mayr, K.; Goller, C. 35 1994 ATP and presentation service for Mizar formalizations. Zbl 1260.68380 Urban, Josef; Rudnicki, Piotr; Sutcliffe, Geoff 35 2013 Productive use of failure in inductive proof. Zbl 0847.68103 Ireland, Andrew; Bundy, Alan 34 1996 MizAR 40 for Mizar 40. Zbl 1356.68191 Kaliszyk, Cezary; Urban, Josef 34 2015 Set theory for verification. I: From foundations to functions. Zbl 0802.68128 Paulson, Lawrence C. 33 1993 IMPS: An interactive mathematical proof system. Zbl 0802.68129 Farmer, William M.; Guttman, Joshua D.; Thayer, F. Javier 33 1993 A formally verified compiler back-end. Zbl 1185.68215 Leroy, Xavier 32 2009 Using typed lambda calculus to implement formal systems on a machine. Zbl 0784.68072 Avron, Arnon; Honsell, Furio; Mason, Ian A.; Pollack, Robert 32 1992 Model-theoretic methods in combined constraint satisfiability. Zbl 1069.03008 Ghilardi, Silvio 31 2004 Explicit representation of terms defined by counter examples. Zbl 0641.68124 Lassez, J.-L.; Marriott, K. 30 1987 lean\(T^ AP\): Lean tableau-based deduction. Zbl 0838.68097 Beckert, Bernhard; Posegga, Joachim 30 1995 Eliminating dublication with the hyper-linking strategy. Zbl 0784.68077 Lee, Shie-Jue; Plaisted, David A. 29 1992 Stochastic Boolean satisfiability. Zbl 0988.68189 Littman, Michael L.; Majercik, Stephen M.; Pitassi, Toniann 27 2001 Backdoor sets of quantified Boolean formulas. Zbl 1191.68353 Samer, Marko; Szeider, Stefan 27 2009 Deduction in non-Horn databases. Zbl 0614.68072 Yahya, Adnan; Henschen, Lawrence J. 27 1985 Experiments with discrimination-tree indexing and path indexing for term retrieval. Zbl 0781.68101 McCune, William 27 1992 An algorithm to evaluate quantified Boolean formulae and its experimental evaluation. Zbl 1002.68165 Cadoli, Marco; Schaerf, Marco; Giovanardi, Andrea; Giovanardi, Massimo 27 2002 Non-Horn clause logic programming without contrapositives. Zbl 0666.68091 Plaisted, David A. 26 1988 Logical cryptanalysis as a SAT problem: Encoding and analysis of the U. S. Data Encryption Standard. Zbl 0968.68052 Massacci, Fabio; Marraro, Laura 26 2000 A Skeptic’s approach to combining HOL and Maple. Zbl 0916.68142 Harrison, J.; Théry, L. 26 1998 Computing circumscription revisited: A reduction algorithm. Zbl 0939.03033 Doherty, Patrick; Łukaszewicz, Witold; Szałas, Andrzej 26 1997 Analyzing program termination and complexity automatically with AProVE. Zbl 1409.68255 Giesl, Jürgen; Aschermann, Cornelius; Brockschmidt, Marc; Emmes, Fabian; Frohn, Florian; Fuhs, Carsten; Hensel, Jera; Otto, Carsten; Plücker, Martin; Schneider-Kamp, Peter; Ströder, Thomas; Swiderski, Stephanie; Thiemann, René 26 2017 Automated theorem proving in GeoGebra: current achievements. Zbl 1356.68181 Botana, Francisco; Hohenwarter, Markus; Janičić, Predrag; Kovács, Zoltán; Petrović, Ivan; Recio, Tomás; Weitzhofer, Simon 26 2015 The locally nameless representation. Zbl 1260.68368 Charguéraud, Arthur 26 2012 Some lambda calculus and type theory formalized. Zbl 0940.03019 McKinna, James; Pollack, Robert 25 1999 Mechanically proving termination using polynomial interpretations. Zbl 1108.03017 Contejean, Evelyne; Marché, Claude; Tomás, Ana Paula; Urbain, Xavier 25 2005 Closed-form upper bounds in static cost analysis. Zbl 1213.68200 Albert, Elvira; Arenas, Puri; Genaim, Samir; Puebla, Germán 24 2011 Ordered semantic hyper-linking. Zbl 0959.68115 Plaisted, David A.; Zhu, Yunshan 24 2000 Complexity of unification problems with associative-commutative operators. Zbl 0781.68076 Kapur, Deepak; Narendran, Paliath 24 1992 A graphical user interface for formal proofs in geometry. Zbl 1131.68094 Narboux, Julien 24 2007 Implicit induction in conditional theories. Zbl 0819.68114 Bouhoula, Adel; Rusinowitch, Michaël 23 1995 Mechanized semantics for the clight subset of the C language. Zbl 1185.68136 Blazy, Sandrine; Leroy, Xavier 23 2009 From bisimulation to simulation: Coarsest partition problems. Zbl 1081.68052 Gentilini, R.; Piazza, C.; Policriti, A. 23 2003 MPTP-motivation, implementation, first experiments. Zbl 1075.68081 Urban, Josef 23 2004 The ILTP problem library for intuitionistic logic. Zbl 1113.68093 Raths, Thomas; Otten, Jens; Kreitz, Christoph 22 2007 New worst-case upper bounds for SAT. Zbl 0960.03009 Hirsch, Edward A. 22 2000 Branching rules for satisfiability. Zbl 0838.68098 Hooker, J. N.; Vinay, V. 22 1995 Testing positiveness of polynomials. Zbl 0916.68084 Hong, Hoon; Jakuš, Dalibor 22 1998 Combining nonstably infinite theories. Zbl 1108.03014 Tinelli, Cesare; Zarba, Calogero G. 22 2005 Gentzen-type systems, resolution and tableaux. Zbl 0788.03013 Avron, Arnon 22 1993 Using hints to increase the effectiveness of an automated reasoning program: Case studies. Zbl 0857.68095 Veroff, Robert 22 1996 A two-level logic approach to reasoning about computations. Zbl 1290.68088 Gacek, Andrew; Miller, Dale; Nadathur, Gopalan 22 2012 First-order modal tableaux. Zbl 0648.03004 Fitting, Melvin 21 1988 On the declarative and procedural semantics of logic programs. Zbl 0681.68109 Przymusinski, Teodor C. 21 1989 A deductive database approach to automated geometry theorem proving and discovering. Zbl 0961.68121 Chou, Shang-Ching; Gao, Xiao-Shan; Zhang, Jing-Zhong 21 2000 A logic for reasoning with inconsistency. Zbl 0807.03019 Kifer, Michael; Lozinskii, Eliezer L. 21 1992 The area method. A recapitulation. Zbl 1242.68281 Janičić, Predrag; Narboux, Julien; Quaresma, Pedro 21 2012 Hybrid. A definitional two-level approach to reasoning with higher-order abstract syntax. Zbl 1252.68252 Felty, Amy; Momigliano, Alberto 21 2012 Short single axioms for Boolean algebra. Zbl 1014.06012 McCune, William; Veroff, Robert; Fitelson, Branden; Harris, Kenneth; Feist, Andrew; Wos, Larry 21 2002 The incredible ELK. From polynomial procedures to efficient reasoning with \(\mathcal {EL}\) ontologies. Zbl 1331.68216 Kazakov, Yevgeny; Krötzsch, Markus; Simančík, František 21 2014 Wave equation numerical resolution: a comprehensive mechanized proof of a C program. Zbl 1267.68208 Boldo, Sylvie; Clément, François; Filliâtre, Jean-Christophe; Mayero, Micaela; Melquiond, Guillaume; Weis, Pierre 21 2013 Hammer for Coq: automation for dependent type theory. Zbl 1448.68458 Czajka, Łukasz; Kaliszyk, Cezary 21 2018 Unification in abelian semigroups. Zbl 0637.68106 Herold, Alexander; Siekmann, Jörg H. 20 1987 Local search algorithms for SAT: an empirical evaluation. Zbl 0961.68039 Hoos, Holger H.; Stützle, Thomas 20 2000 Priorities on defaults with prerequisites, and their application in treating specificity in terminological default logic. Zbl 0842.68081 Baader, Franz; Hollunder, Bernhard 20 1995 Exponential lower bounds for the running time of DPLL algorithms on satisfiable formulas. Zbl 1109.68098 Alekhnovich, Michael; Hirsch, Edward A.; Itsykson, Dmitry 20 2005 Debugging incoherent terminologies. Zbl 1132.68740 Schlobach, Stefan; Huang, Zhisheng; Cornet, Ronald; van Harmelen, Frank 20 2007 On deciding satisfiability by theorem proving with speculative inferences. Zbl 1243.68265 Bonacina, Maria Paola; Lynch, Christopher A.; de Moura, Leonardo 20 2011 Conjecture synthesis for inductive theories. Zbl 1243.68268 Johansson, Moa; Dixon, Lucas; Bundy, Alan 20 2011 Autarkic computations in formal proofs. Zbl 1002.68156 Barendregt, Henk; Barendsen, Erik 20 2002 The theory of idempotent semigroups is of unification type zero. Zbl 0626.68070 Baader, Franz 19 1986 Deciding Boolean algebra with Presburger arithmetic. Zbl 1112.03011 Kuncak, Viktor; Nguyen, Huu Hai; Rinard, Martin 19 2006 TPS: A theorem-proving system for classical type theory. Zbl 0858.03017 Andrews, Peter B.; Bishop, Matthew; Issar, Sunil; Nesmith, Dan; Pfenning, Frank; Xi, Hongwei 19 1996 Complexity and resource bound analysis of imperative programs using difference constraints. Zbl 1409.68076 Sinn, Moritz; Zuleger, Florian; Veith, Helmut 19 2017 The higher-order prover Leo-II. Zbl 1356.68176 Benzmüller, Christoph; Sultana, Nik; Paulson, Lawrence C.; Theiß, Frank 19 2015 Proof Pearl: regular expression equivalence and relation algebra. Zbl 1269.68090 Krauss, Alexander; Nipkow, Tobias 19 2012 A framework for proof systems. Zbl 1242.03057 Nigam, Vivek; Miller, Dale 19 2010 The Mizar Mathematical Library in OMDoc: translation and applications. Zbl 1260.68375 Iancu, Mihnea; Kohlhase, Michael; Rabe, Florian; Urban, Josef 19 2013 Rensets and renaming-based recursion for syntax with bindings extended version. Zbl 07722430 Popescu, Andrei 1 2023 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 Integrating Owicki-Gries for C11-style memory models into Isabelle/HOL. Zbl 07498610 Dalvandi, Sadegh; Dongol, Brijesh; Doherty, Simon; Wehrheim, Heike 4 2022 Predicate transformer semantics for hybrid systems. Verification components for Isabelle/HOL. Zbl 07498609 Huerta y Munive, Jonathan Julián; Struth, Georg 3 2022 A Coq formalization of Lebesgue integration of nonnegative functions. Zbl 07538894 Boldo, Sylvie; Clément, François; Faissole, Florian; Martin, Vincent; Mayero, Micaela 2 2022 Analyzing read-once cutting plane proofs in Horn systems. Zbl 07538896 Wojciechowski, Piotr; Subramani, K.; Chandrasekaran, R. 1 2022 Larry Wos: visions of automated reasoning. Zbl 1511.68005 Beeson, Michael; Bonacina, Maria Paola; Kinyon, Michael; Sutcliffe, Geoff 1 2022 Making higher-order superposition work. Zbl 1512.68432 Vukmirović, Petar; Bentkamp, Alexander; Blanchette, Jasmin; Cruanes, Simon; Nummelin, Visa; Tourret, Sophie 1 2022 A Wos challenge met. Zbl 1512.68430 Veroff, Robert 1 2022 A mechanized proof of the max-flow min-cut theorem for countable networks with applications to probability theory. Zbl 1512.05165 Lochbihler, Andreas 1 2022 Theorem proving as constraint solving with coherent logic. Zbl 1511.68316 Janičić, Predrag; Narboux, Julien 1 2022 Verifying Whiley programs with Boogie. Zbl 1512.68059 Pearce, David J.; Utting, Mark; Groves, Lindsay 1 2022 Towards formalising Schutz’ axioms for Minkowski spacetime in Isabelle/HOL. Zbl 1511.68331 Schmoetten, Richard; Palmer, Jake E.; Fleuriot, Jacques D. 1 2022 Formalization of the computational theory of a Turing complete functional language model. Zbl 1511.68338 Ramos, Thiago Mendonça Ferreira; Almeida, Ariane Alves; Ayala-Rincón, Mauricio 1 2022 Combination of uniform interpolants via Beth definability. Zbl 07606344 Calvanese, Diego; Ghilardi, Silvio; Gianola, Alessandro; Montali, Marco; Rivkin, Andrey 1 2022 Conflict-driven satisfiability for theory combination: lemmas, modules, and proofs. Zbl 07498608 Bonacina, Maria Paola; Graham-Lengrand, Stéphane; Shankar, Natarajan 1 2022 Superposition with lambdas. Zbl 07433023 Bentkamp, Alexander; Blanchette, Jasmin; Tourret, Sophie; Vukmirović, Petar; Waldmann, Uwe 7 2021 TacticToe: learning to prove with tactics. Zbl 07356973 Gauthier, Thibault; Kaliszyk, Cezary; Urban, Josef; Kumar, Ramana; Norrish, Michael 7 2021 Automated proof of Bell-LaPadula security properties. Zbl 07356979 Cristiá, Maximiliano; Rossi, Gianfranco 7 2021 Extensional higher-order paramodulation in Leo-III. Zbl 1509.68321 Steen, Alexander; Benzmüller, Christoph 5 2021 Automated reasoning with restricted intensional sets. Zbl 07432188 Cristiá, Maximiliano; Rossi, Gianfranco 5 2021 Building strategies into QBF proofs. Zbl 07356969 Beyersdorff, Olaf; Blinkhorn, Joshua; Mahajan, Meena 4 2021 An automatically verified prototype of the Tokeneer ID station specification. Zbl 07461267 Cristiá, Maximiliano; Rossi, Gianfranco 4 2021 Machine learning guidance for connection tableaux. Zbl 07356974 Färber, Michael; Kaliszyk, Cezary; Urban, Josef 3 2021 On the importance of domain model configuration for automated planning engines. Zbl 07432186 Vallati, Mauro; Chrpa, Lukáš; McCluskey, Thomas Leo; Hutter, Frank 2 2021 Model completeness, uniform interpolants and superposition calculus. (With applications to verification of data-aware processes). Zbl 07433024 Calvanese, Diego; Ghilardi, Silvio; Gianola, Alessandro; Montali, Marco; Rivkin, Andrey 2 2021 Experiences from exporting major proof assistant libraries. Zbl 07461271 Kohlhase, Michael; Rabe, Florian 2 2021 Certified quantum computation in Isabelle/HOL. Zbl 07432184 Bordg, Anthony; Lachnitt, Hanna; He, Yijun 1 2021 Automated discovery of geometric theorems based on vector equations. Zbl 07432185 Peng, Xicheng; Chen, Qihang; Zhang, Jingzhong; Chen, Mao 1 2021 Optimization modulo the theories of signed bit-vectors and floating-point numbers. Zbl 07433028 Trentin, Patrick; Sebastiani, Roberto 1 2021 Formalization of Euler-Lagrange equation set based on variational calculus in HOL light. Zbl 07356966 Guan, Yong; Zhang, Jingzhi; Wang, Guohui; Li, Ximeng; Shi, Zhiping; Li, Yongdong 1 2021 Formalization of the Poincaré disc model of hyperbolic geometry. Zbl 07356967 Simić, Danijela; Marić, Filip; Boutry, Pierre 1 2021 Unbounded-time safety verification of guarded LTI models with inputs by abstract acceleration. Zbl 07356971 Cattaruzza, Dario; Abate, Alessandro; Schrammel, Peter; Kroening, Daniel 1 2021 Decidable \({\exists}^*{\forall}^*\) first-order fragments of linear rational arithmetic with uninterpreted predicates. Zbl 07356976 Voigt, Marco 1 2021 Higher-order quantifier elimination, counter simulations and fault-tolerant systems. Zbl 07356977 Ghilardi, Silvio; Pagani, Elena 1 2021 Human-centered automated proof search. Zbl 07461268 Sieg, Wilfried; Derakhshan, Farzaneh 1 2021 Formalization of ring theory in PVS. Isomorphism theorems, principal, prime and maximal ideals, Chinese remainder theorem. Zbl 1493.68389 de Lima, Thaynara Arielly; Galdino, André Luiz; Avelar, Andréia Borges; Ayala-Rincón, Mauricio 1 2021 ICE-based refinement type discovery for higher-order functional programs. Zbl 1468.68059 Champion, Adrien; Chiba, Tomoya; Kobayashi, Naoki; Sato, Ryosuke 8 2020 Solving quantifier-free first-order constraints over finite sets and binary relations. Zbl 1468.03009 Cristiá, Maximiliano; Rossi, Gianfranco 8 2020 OptiMathSAT: a tool for optimization modulo theories. Zbl 1468.68206 Sebastiani, Roberto; Trentin, Patrick 8 2020 Strong extension-free proof systems. Zbl 1468.03011 Heule, Marijn J. H.; Kiesl, Benjamin; Biere, Armin 8 2020 A verified implementation of the Berlekamp-Zassenhaus factorization algorithm. Zbl 1469.68165 Divasón, Jose; Joosten, Sebastiaan J. C.; Thiemann, René; Yamada, Akihisa 8 2020 The MetaCoq project. Zbl 1468.68075 Sozeau, Matthieu; Anand, Abhishek; Boulier, Simon; Cohen, Cyril; Forster, Yannick; Kunze, Fabian; Malecha, Gregory; Tabareau, Nicolas; Winterhalter, Théo 7 2020 \(\mathrm{K}_{\mathrm S}\mathrm{P}\) a resolution-based theorem prover for \({\mathsf{K}}_n\): architecture, refinements, strategies and experiments. Zbl 1468.68304 Nalon, Cláudia; Hustadt, Ullrich; Dixon, Clare 7 2020 Exploring the structure of an algebra text with locales. Zbl 1468.68277 Ballarin, Clemens 6 2020 Efficient verified (UN)SAT certificate checking. Zbl 1468.68134 Lammich, Peter 6 2020 Conflict-driven satisfiability for theory combination: transition system and completeness. Zbl 1468.68194 Bonacina, Maria Paola; Graham-Lengrand, Stéphane; Shankar, Natarajan 6 2020 A formalized general theory of syntax with bindings: extended version. Zbl 1468.68073 Gheri, Lorenzo; Popescu, Andrei 6 2020 Formalizing Bachmair and Ganzinger’s ordered resolution prover. Zbl 1468.68307 Schlichtkrull, Anders; Blanchette, Jasmin; Traytel, Dmitriy; Waldmann, Uwe 5 2020 Combining induction and saturation-based theorem proving. Zbl 1476.68300 Echenim, M.; Peltier, N. 5 2020 Scalable fine-grained proofs for formula processing. Zbl 1468.68278 Barbosa, Haniel; Blanchette, Jasmin Christian; Fleury, Mathias; Fontaine, Pascal 5 2020 Probably partially true: satisfiability for Łukasiewicz infinitely-valued probabilistic logic and related topics. Zbl 1468.68200 Finger, Marcelo; Preto, Sandro 4 2020 Politeness and combination methods for theories with bridging functions. Zbl 1468.68143 Chocron, Paula; Fontaine, Pascal; Ringeissen, Christophe 4 2020 Using well-founded relations for proving operational termination. Zbl 1468.03034 Lucas, Salvador 4 2020 Blocking and other enhancements for bottom-up model generation methods. Zbl 1468.68279 Baumgartner, Peter; Schmidt, Renate A. 4 2020 Automatically verifying temporal properties of pointer programs with cyclic proof. Zbl 1468.68137 Tellez, Gadi; Brotherston, James 4 2020 System-level non-interference of constant-time cryptography. II: Verified static analysis and stealth memory. Zbl 1459.68027 Barthe, Gilles; Betarte, Gustavo; Campo, Juan Diego; Luna, Carlos; Pichardie, David 4 2020 Verified analysis of random binary tree structures. Zbl 1468.68289 Eberl, Manuel; Haslbeck, Max W.; Nipkow, Tobias 3 2020 First-order automated reasoning with theories: when deduction modulo theory meets practice. Zbl 1468.68282 Burel, Guillaume; Bury, Guillaume; Cauderlier, Raphaël; Delahaye, David; Halmagrand, Pierre; Hermant, Olivier 3 2020 Multi-cost bounded tradeoff analysis in MDP. Zbl 1468.68132 Hartmanns, Arnd; Junges, Sebastian; Katoen, Joost-Pieter; Quatmann, Tim 3 2020 Evaluating winding numbers and counting complex roots through Cauchy indices in Isabelle/HOL. Zbl 1468.68299 Li, Wenda; Paulson, Lawrence C. 3 2020 The 2D dependency pair framework for conditional rewrite systems. II: Advanced processors and implementation techniques. Zbl 1459.68092 Lucas, Salvador; Meseguer, José; Gutiérrez, Raúl 3 2020 Loop-type sequent calculi for temporal logic. Zbl 1462.03012 Alonderis, R.; Pliuškevičius, R.; Pliuškevičienė, A.; Giedra, H. 3 2020 Simulating strong practical proof systems with extended resolution. Zbl 1468.68293 Kiesl, Benjamin; Rebola-Pardo, Adrián; Heule, Marijn J. H.; Biere, Armin 2 2020 Automating free logic in HOL, with an experimental application in category theory. Zbl 1434.68639 Benzmüller, Christoph; Scott, Dana S. 2 2020 A verified implementation of algebraic numbers in Isabelle/HOL. Zbl 1468.68326 Joosten, Sebastiaan J. C.; Thiemann, René; Yamada, Akihisa 2 2020 Graph theory in Coq: minors, treewidth, and isomorphisms. Zbl 1468.68320 Doczkal, Christian; Pous, Damien 1 2020 A library for formalization of linear error-correcting codes. Zbl 1468.68314 Affeldt, Reynald; Garrigue, Jacques; Saikawa, Takafumi 1 2020 Constructive decision via redundancy-free proof-search. Zbl 1468.03015 Larchey-Wendling, Dominique 1 2020 Parameterized model checking on the TSO weak memory model. Zbl 1468.68123 Conchon, Sylvain; Declerck, David; Zaïdi, Fatiha 1 2020 Fine-grained complexity of safety verification. Zbl 1468.68121 Chini, Peter; Meyer, Roland; Saivasan, Prakash 1 2020 A learning-based approach to synthesizing invariants for incomplete verification engines. Zbl 1468.68074 Neider, Daniel; Madhusudan, P.; Saha, Shambwaditya; Garg, Pranav; Park, Daejun 1 2020 Limited second-order functionality in a first-order setting. Zbl 1468.68291 Kaufmann, Matt; Moore, J Strother 1 2020 From types to sets by local type definition in higher-order logic. Zbl 1468.68295 Kunčar, Ondřej; Popescu, Andrei 11 2019 Verifying the correctness and amortized complexity of a union-find implementation in separation logic with time credits. Zbl 1468.68120 Charguéraud, Arthur; Pottier, François 10 2019 Refinement to imperative HOL. Zbl 1465.68291 Lammich, Peter 9 2019 The univalence axiom in cubical sets. Zbl 1506.03064 Bezem, Marc; Coquand, Thierry; Huber, Simon 8 2019 Canonicity for cubical type theory. Zbl 1477.03036 Huber, Simon 8 2019 Parallel postulates and continuity axioms: a mechanized study in intuitionistic logic using Coq. Zbl 1441.03011 Boutry, Pierre; Gries, Charly; Narboux, Julien; Schreck, Pascal 7 2019 A consistent foundation for Isabelle/HOL. Zbl 1465.68289 Kunčar, Ondřej; Popescu, Andrei 7 2019 Formalizing network flow algorithms: a refinement approach in Isabelle/HOL. Zbl 1468.68328 Lammich, Peter; Sefidgar, S. Reza 6 2019 Guarded cubical type theory. Zbl 1477.03034 Birkedal, Lars; Bizjak, Aleš; Clouston, Ranald; Grathwohl, Hans Bugge; Spitters, Bas; Vezzosi, Andrea 6 2019 Semantics of Mizar as an Isabelle object logic. Zbl 1468.68290 Kaliszyk, Cezary; Pąk, Karol 6 2019 A proof theory for model checking. Zbl 1468.03078 Heath, Quentin; Miller, Dale 5 2019 Efficient active automata learning via mutation testing. Zbl 1468.68117 Aichernig, Bernhard K.; Tappler, Martin 5 2019 Formalization of metatheory of the Quipper quantum programming language in a linear logic. Zbl 1468.68330 Mahmoud, Mohamed Yousri; Felty, Amy P. 4 2019 Verifying OpenJDK’s sort method for generic collections. Zbl 1468.68125 de Gouw, Stijn; de Boer, Frank S.; Bubel, Richard; Hähnle, Reiner; Rot, Jurriaan; Steinhöfel, Dominic 4 2019 The flow of ODEs: formalization of variational equation and Poincaré map. Zbl 1468.68325 Immler, Fabian; Traut, Christoph 4 2019 Fast formal proof of the Erdős-Szekeres conjecture for convex polygons with at most 6 points. Zbl 1468.68302 Marić, Filip 4 2019 The James construction and \(\pi _4(\mathbb{S}^{3})\) in homotopy type theory. Zbl 1477.03035 Brunerie, Guillaume 4 2019 Formally verifying the solution to the Boolean Pythagorean triples problem. Zbl 1468.68318 Cruz-Filipe, Luís; Marques-Silva, Joao; Schneider-Kamp, Peter 4 2019 QPCF: higher-order languages and quantum circuits. Zbl 1468.68049 Paolini, Luca; Piccolo, Mauro; Zorzi, Margherita 3 2019 Compositional falsification of cyber-physical systems with machine learning components. Zbl 1468.68126 Dreossi, Tommaso; Donzé, Alexandre; Seshia, Sanjit A. 3 2019 Formally verified approximations of definite integrals. Zbl 1468.68301 Mahboubi, Assia; Melquiond, Guillaume; Sibut-Pinote, Thomas 3 2019 Amortized complexity verified. Zbl 1465.68060 Nipkow, Tobias; Brinkop, Hauke 3 2019 A verified CompCert front-end for a memory model supporting pointer arithmetic and uninitialised data. Zbl 1465.68041 Besson, Frédéric; Blazy, Sandrine; Wilke, Pierre 3 2019 System-level non-interference of constant-time cryptography. I: Model. Zbl 1459.68026 Barthe, Gilles; Betarte, Gustavo; Campo, Juan Diego; Luna, Carlos 3 2019 Long-distance Q-resolution with dependency schemes. Zbl 1459.68229 Peitl, Tomáš; Slivovsky, Friedrich; Szeider, Stefan 3 2019 From signatures to monads in UniMath. Zbl 1468.03007 Ahrens, Benedikt; Matthes, Ralph; Mörtberg, Anders 3 2019 A formalization of convex polyhedra based on the simplex method. Zbl 1468.68316 Allamigeon, Xavier; Katz, Ricardo D. 3 2019 ...and 748 more Documents all cited Publications top 5 cited Publications all top 5 Cited by 4,739 Authors 45 Paulson, Lawrence Charles 43 Urban, Josef 34 Kaliszyk, Cezary 30 Blanchette, Jasmin Christian 30 Eiter, Thomas 28 Baader, Franz 28 Benzmüller, Christoph Ewald 28 Meseguer Guaita, José 27 Lucas, Salvador 27 Weidenbach, Christoph 25 Middeldorp, Aart 24 Grabowski, Adam 23 Giesl, Jürgen 22 Bonacina, Maria Paola 22 Gao, Xiaoshan 22 Marques-Silva, João P. 22 Platzer, André 21 Korniłowicz, Artur 21 Nipkow, Tobias 21 Rabe, Florian 21 Sutcliffe, Geoff 21 Voronkov, Andrei 20 Ayala-Rincón, Mauricio 20 Ghilardi, Silvio 20 Subramani, Krishnan 20 Tinelli, Cesare 19 Kapur, Deepak 19 Thiemann, René 18 Heule, Marijn J. H. 18 Koch, Sebastian 18 Peltier, Nicolas 17 Cantone, Domenico 17 Pąk, Karol 17 Waldmann, Uwe 16 Barrett, Clark W. 16 Biere, Armin 16 Calvanese, Diego 16 Gottlob, Georg 16 Janičić, Predrag 16 Schaub, Torsten H. 16 Schneider-Kamp, Peter 15 Bundy, Alan 15 Kohlhase, Michael 15 Moser, Georg 15 Szeider, Stefan 14 Baumgartner, Peter 14 Dowek, Gilles 14 Nakasho, Kazuhisa 14 Narboux, Julien 14 Naumowicz, Adam 14 Plaisted, David Alan 14 Reger, Giles 14 Reynolds, Andrew 14 Ringeissen, Christophe 14 Smolka, Gert 14 Wos, Larry 13 Dixon, Clare 13 Fernández, Maribel 13 Kovács, Zoltán 13 Kutsia, Temur 13 Pimentel, Elaine 13 Recio, Tomas 13 Rusinowitch, Michaël 13 Shidama, Yasunari 13 Subrahmanian, V. S. 13 Tahar, Sofiène 13 Tourret, Sophie 13 Wang, Dongming 13 Winkler, Sarah 13 Zhang, Hantao 12 Alviano, Mario 12 Bentkamp, Alexander 12 Bonatti, Piero Andrea 12 Botana, Francisco 12 Chou, Shangching 12 Goré, Rajeev Prabhakar 12 Gutiérrez, Raúl 12 Horrocks, Ian 12 Kirchner, Claude 12 Kuncak, Viktor 12 Miller, Dale Allen 12 Montanari, Angelo 12 Nigam, Vivek 12 Pientka, Brigitte 12 Popescu, Andrei 12 Schmidt-Schauß, Manfred 12 Schwarzweller, Christoph 12 Sebastiani, Roberto 12 Struth, Georg 12 Wolter, Frank 12 Zakharyaschev, Michael Viktorovich 11 Amgoud, Leila 11 Brown, Chad Edward 11 Felty, Amy P. 11 Fuhs, Carsten 11 Gabbay, Dov M. 11 Giunchiglia, Enrico 11 Jakubův, Jan 11 Lochbihler, Andreas 11 Maratea, Marco ...and 4,639 more Authors all top 5 Cited in 243 Journals 522 Journal of Automated Reasoning 215 Artificial Intelligence 190 Theoretical Computer Science 127 Journal of Symbolic Computation 127 Annals of Mathematics and Artificial Intelligence 118 Formalized Mathematics 80 Information and Computation 67 Theory and Practice of Logic Programming 60 MSCS. Mathematical Structures in Computer Science 54 Logical Methods in Computer Science 47 Formal Aspects of Computing 46 International Journal of Approximate Reasoning 43 Journal of Applied Logic 43 Journal of Logical and Algebraic Methods in Programming 41 Journal of Applied Non-Classical Logics 37 Annals of Pure and Applied Logic 36 Formal Methods in System Design 32 Discrete Applied Mathematics 30 Journal of Functional Programming 29 Mathematics in Computer Science 26 Constraints 26 ACM Transactions on Computational Logic 25 Information Processing Letters 25 Information Sciences 22 Fuzzy Sets and Systems 22 Journal of Computer and System Sciences 22 Studia Logica 18 Applied Mathematics and Computation 16 Acta Informatica 15 Computers & Mathematics with Applications 14 Applicable Algebra in Engineering, Communication and Computing 14 Journal of Systems Science and Complexity 13 New Generation Computing 13 Logica Universalis 12 The Journal of Symbolic Logic 11 Synthese 11 AI Communications 11 Fundamenta Informaticae 11 The Journal of Logic and Algebraic Programming 10 Journal of Computer Science and Technology 9 Journal of Philosophical Logic 9 Journal of Logic, Language and Information 9 The Journal of Artificial Intelligence Research (JAIR) 8 Science of Computer Programming 8 International Journal of Computer Mathematics 8 The Bulletin of Symbolic Logic 8 Soft Computing 7 Automatica 7 Notre Dame Journal of Formal Logic 7 JETAI. Journal of Experimental & Theoretical Artificial Intelligence 7 Computational Geometry 6 International Journal of General Systems 6 Mathematics and Computers in Simulation 6 Computers & Operations Research 6 Machine Learning 6 European Journal of Operational Research 6 Archive for Mathematical Logic 6 Computer Languages, Systems & Structures 6 Journal of Satisfiability, Boolean Modeling and Computation 6 The Review of Symbolic Logic 5 Algorithmica 5 International Journal of Intelligent Systems 5 Annals of Operations Research 5 Theory of Computing Systems 5 Higher-Order and Symbolic Computation 5 Journal of Formalized Reasoning 5 Philosophical Transactions of the Royal Society of London. A. Mathematical, Physical and Engineering Sciences 5 Prikladnaya Diskretnaya Matematika 4 Communications in Algebra 4 Mathematical and Computer Modelling 4 International Journal of Foundations of Computer Science 4 Indagationes Mathematicae. New Series 4 Computational Complexity 4 Journal of Mathematical Sciences (New York) 4 Journal of Combinatorial Optimization 4 LMS Journal of Computation and Mathematics 4 Journal of Applied Mathematics 4 Nonlinear Analysis. Hybrid Systems 4 Revista de la Real Academia de Ciencias Exactas, Físicas y Naturales. Serie A: Matemáticas. RACSAM 3 Mathematics of Computation 3 Journal of Algebra 3 Semigroup Forum 3 Science in China. Series A 3 Experimental Mathematics 3 Mathematical Logic Quarterly (MLQ) 3 Journal of Heuristics 3 Mathematical Problems in Engineering 3 Communications in Nonlinear Science and Numerical Simulation 3 International Journal of Applied Mathematics and Computer Science 3 RAIRO. Theoretical Informatics and Applications 3 Journal of Discrete Algorithms 3 Lietuvos Matematikos Rinkinys. Proceedings of the Lithuanian Mathematical Society. Series A 2 Discrete Mathematics 2 Journal of Mathematical Physics 2 The Mathematical Intelligencer 2 Computing 2 Journal of Computational and Applied Mathematics 2 Journal of Mathematical Economics 2 Journal of Pure and Applied Algebra 2 Programming and Computer Software ...and 143 more Journals all top 5 Cited in 53 Fields 3,639 Computer science (68-XX) 1,485 Mathematical logic and foundations (03-XX) 123 Operations research, mathematical programming (90-XX) 108 Information and communication theory, circuits (94-XX) 81 Geometry (51-XX) 73 Numerical analysis (65-XX) 68 Combinatorics (05-XX) 57 Commutative algebra (13-XX) 56 Order, lattices, ordered algebraic structures (06-XX) 52 Number theory (11-XX) 52 Systems theory; control (93-XX) 44 Group theory and generalizations (20-XX) 43 Game theory, economics, finance, and other social and behavioral sciences (91-XX) 36 Category theory; homological algebra (18-XX) 34 Field theory and polynomials (12-XX) 33 Algebraic geometry (14-XX) 29 General and overarching topics; collections (00-XX) 28 Real functions (26-XX) 25 History and biography (01-XX) 24 General algebraic systems (08-XX) 23 Algebraic topology (55-XX) 21 Ordinary differential equations (34-XX) 17 Linear and multilinear algebra; matrix theory (15-XX) 17 Biology and other natural sciences (92-XX) 15 Quantum theory (81-XX) 15 Mathematics education (97-XX) 14 Probability theory and stochastic processes (60-XX) 13 Statistics (62-XX) 11 Associative rings and algebras (16-XX) 9 Partial differential equations (35-XX) 9 Dynamical systems and ergodic theory (37-XX) 9 Operator theory (47-XX) 9 Convex and discrete geometry (52-XX) 8 Measure and integration (28-XX) 8 Mechanics of particles and systems (70-XX) 7 Special functions (33-XX) 7 Functional analysis (46-XX) 5 Nonassociative rings and algebras (17-XX) 5 Calculus of variations and optimal control; optimization (49-XX) 4 Optics, electromagnetic theory (78-XX) 4 Relativity and gravitational theory (83-XX) 3 Functions of a complex variable (30-XX) 3 Sequences, series, summability (40-XX) 3 Approximations and expansions (41-XX) 3 Harmonic analysis on Euclidean spaces (42-XX) 3 Differential geometry (53-XX) 3 General topology (54-XX) 2 Difference and functional equations (39-XX) 2 Integral equations (45-XX) 2 Fluid mechanics (76-XX) 1 Several complex variables and analytic spaces (32-XX) 1 Mechanics of deformable solids (74-XX) 1 Geophysics (86-XX) Citations by Year