×

zbMATH — the first resource for mathematics

Journal of Automated Reasoning

Short Title: J. Autom. Reasoning
Publisher: Springer Netherlands, Dordrecht
ISSN: 0168-7433; 1573-0670/e
Online: http://link.springer.com/journal/volumesAndIssues/10817
Comments: Indexed cover-to-cover
Documents Indexed: 1,055 Publications (since 1985)
References Indexed: 719 Publications with 24,011 References.
all top 5

Latest Issues

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)
43, No. 4 (2009)
43, No. 3 (2009)
43, No. 2 (2009)
43, No. 1 (2009)
42, No. 2-4 (2009)
42, No. 1 (2009)
41, No. 3-4 (2008)
41, No. 2 (2008)
41, No. 1 (2008)
40, No. 4 (2008)
40, No. 2-3 (2008)
40, No. 1 (2008)
39, No. 4 (2007)
...and 112 more Volumes
all top 5

Authors

38 Wos, Larry
19 Paulson, Lawrence Charles
13 Blanchette, Jasmin Christian
12 Urban, Josef
11 Bundy, Alan
11 Chou, Shangching
11 Giesl, Jürgen
11 McCune, William W.
11 Nipkow, Tobias
11 Sutcliffe, Geoff
10 Peltier, Nicolas
10 Plaisted, David Alan
9 Gao, Xiaoshan
8 Kaliszyk, Cezary
8 Kaufmann, Matt
8 Moore, J Strother
8 Norrish, Michael
8 Veroff, Robert
7 Bonacina, Maria Paola
7 Cantone, Domenico
7 Kapur, Deepak
7 Lammich, Peter
7 Leroy, Xavier
7 Schneider-Kamp, Peter
6 Baumgartner, Peter
6 Blazy, Sandrine
6 Felty, Amy P.
6 Middeldorp, Aart
6 Policriti, Alberto
6 Rusinowitch, Michaël
6 Stickel, Mark E.
6 Thiemann, René
6 Walsh, Toby
6 Yahya, Adnan H.
6 Zhang, Hantao
5 Avigad, Jeremy
5 Basin, David A.
5 Biere, Armin
5 de Moura, Leonardo
5 Echenim, Mnacho
5 Hähnle, Reiner
5 Henschen, Lawrence J.
5 Horrocks, Ian
5 Hustadt, Ullrich
5 Kazakov, Yevgeny
5 Kunen, Kenneth
5 Miller, Dale Allen
5 Narendran, Paliath
5 Ohlbach, Hans Jürgen
5 Popescu, Andrei
5 Schmidt, Renate A.
5 Smolka, Gert
5 Subrahmanian, V. S.
5 Weidenbach, Christoph
4 Andrews, Peter B.
4 Barthe, Gilles
4 Bledsoe, Woodrow W.
4 Böhme, Sascha
4 Cialdea Mayer, Marta
4 Delaune, Stéphanie
4 Fiorino, Guido
4 Fitelson, Branden
4 Gamboa, Ruben A.
4 Giunchiglia, Fausto
4 Heule, Marijn J. H.
4 Janičić, Predrag
4 Klein, Gerwin
4 Korniłowicz, Artur
4 Kremer, Steve
4 Lochbihler, Andreas
4 Loveland, Donald W.
4 Lu, James J.
4 Lucas, Salvador
4 Lusk, Ewing L.
4 Martín-Mateos, Francisco-Jesús
4 Melquiond, Guillaume
4 Minker, Jack
4 Motik, Boris
4 Muñoz, César A.
4 Murray, Neil V.
4 Myreen, Magnus O.
4 Narboux, Julien
4 Overbeek, Ross A.
4 Pąk, Karol
4 Pelletier, Francis Jeffry
4 Quaife, Art
4 Rudnicki, Piotr
4 Ruiz-Reina, José-Luis
4 Schulz, Stephan
4 Suttner, Christian B.
4 Szeider, Stefan
4 Théry, Laurent
4 Urban, Christian
4 Voronkov, Andrei
4 Yamada, Akihisa
4 Zarba, Calogero G.
4 Zhang, Jingzhong
3 Alonso, José-Antonio
3 Anantharaman, Siva
3 Appel, Andrew W.
...and 1,347 more Authors
all top 5

Fields

973 Computer science (68-XX)
436 Mathematical logic and foundations (03-XX)
36 General and overarching topics; collections (00-XX)
29 Information and communication theory, circuits (94-XX)
18 Group theory and generalizations (20-XX)
16 Number theory (11-XX)
16 Geometry (51-XX)
15 Operations research, mathematical programming (90-XX)
13 Numerical analysis (65-XX)
10 Order, lattices, ordered algebraic structures (06-XX)
7 History and biography (01-XX)
7 Combinatorics (05-XX)
6 Commutative algebra (13-XX)
6 Category theory; homological algebra (18-XX)
4 Field theory and polynomials (12-XX)
4 Game theory, economics, finance, and other social and behavioral sciences (91-XX)
3 Algebraic geometry (14-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 Algebraic topology (55-XX)
3 Systems theory; control (93-XX)
2 Linear and multilinear algebra; matrix theory (15-XX)
2 Nonassociative rings and algebras (17-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)
2 Probability theory and stochastic processes (60-XX)
2 Quantum theory (81-XX)
1 Associative rings and algebras (16-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 Relativity and gravitational theory (83-XX)
1 Biology and other natural sciences (92-XX)
1 Mathematics education (97-XX)

Publications by Year

Citations contained in zbMATH Open

729 Publications have been cited 5,058 times in 3,111 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
87
2007
The TPTP problem library and associated infrastructure and associated infrastructure. The FOF and CNF parts, v3.5.0. Zbl 1185.68636
Sutcliffe, Geoff
84
2009
The TPTP problem library. CNF release v1. 2. 1. Zbl 0910.68197
Sutcliffe, Geoff; Suttner, Christian
59
1998
Four decades of {Mizar}. Foreword. Zbl 1336.00111
Grabowski, Adam (ed.); Korniłowicz, Artur (ed.); Naumowicz, Adam (ed.)
56
2015
Basic principles of mechanical theorem proving in elementary geometries. Zbl 0642.68163
Wu, Wentsun
56
1986
Theorem proving modulo. Zbl 1049.03011
Dowek, Gilles; Hardin, Thérèse; Kirchner, Claude
48
2003
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
46
2018
Heavy-tailed phenomena in satisfiability and constraint satisfaction problems. Zbl 0967.68145
Gomes, Carla P.; Selman, Bart; Crato, Nuno; Kautz, Henry
44
2000
Nominal techniques in Isabelle/HOL. Zbl 1140.68061
Urban, Christian
44
2008
Solution of the Robbins problem. Zbl 0883.06011
McCune, William
43
1997
The foundation of a generic theorem prover. Zbl 0679.68173
Paulson, Lawrence C.
43
1989
A Prolog technology theorem prover: Implementation by an extended Prolog compiler. Zbl 0662.68104
Stickel, Mark E.
42
1988
SETHEO: A high-performance theorem prover. Zbl 0759.68080
Letz, R.; Schumann, J.; Bayerl, S.; Bibel, W.
42
1992
Automated deduction by theory resolution. Zbl 0616.68076
Stickel, Mark E.
41
1985
Mechanizing and improving dependency pairs. Zbl 1113.68088
Giesl, Jürgen; Thiemann, René; Schneider-Kamp, Peter; Falke, Stephan
41
2006
Algorithms for computing minimal unsatisfiable subsets of constraints. Zbl 1154.68510
Liffiton, Mark H.; Sakallah, Karem A.
39
2008
Matrix interpretations for proving termination of term rewriting. Zbl 1139.68049
Endrullis, Jörg; Waldmann, Johannes; Zantema, Hans
37
2008
Seventy-five problems for testing automatic theorem provers. Zbl 0642.68147
Pelletier, Francis Jeffry
35
1986
Answer set programming based on propositional satisfiability. Zbl 1107.68029
Giunchiglia, Enrico; Lierler, Yuliya; Maratea, Marco
34
2006
A tableau decision procedure for \(\mathcal{SHOIQ}\). Zbl 1132.68734
Horrocks, Ian; Sattler, Ulrike
33
2007
Controlled integration of the cut rule into connection tableau calculi. Zbl 0816.03005
Letz, R.; Mayr, K.; Goller, C.
30
1994
Productive use of failure in inductive proof. Zbl 0847.68103
Ireland, Andrew; Bundy, Alan
30
1996
Inferring from inconsistency in preference-based argumentation frameworks. Zbl 1056.68589
Amgoud, Leila; Cayrol, Claudette
30
2002
IMPS: An interactive mathematical proof system. Zbl 0802.68129
Farmer, William M.; Guttman, Joshua D.; Thayer, F. Javier
28
1993
The HOL Light theory of Euclidean space. Zbl 1260.68373
Harrison, John
28
2013
Using typed lambda calculus to implement formal systems on a machine. Zbl 0784.68072
Avron, Arnon; Honsell, Furio; Mason, Ian A.; Pollack, Robert
27
1992
Deduction in non-Horn databases. Zbl 0614.68072
Yahya, Adnan; Henschen, Lawrence J.
27
1985
Automatic discovery of theorems in elementary geometry. Zbl 0941.03010
Recio, T.; Vélez, M. P.
25
1999
Eliminating dublication with the hyper-linking strategy. Zbl 0784.68077
Lee, Shie-Jue; Plaisted, David A.
25
1992
Differential dynamic logic for hybrid systems. Zbl 1181.03035
Platzer, André
25
2008
Computing circumscription revisited: A reduction algorithm. Zbl 0939.03033
Doherty, Patrick; Łukaszewicz, Witold; Szałas, Andrzej
24
1997
Learning-assisted automated reasoning with \(\mathsf{Flyspeck}\). Zbl 1314.68283
Kaliszyk, Cezary; Urban, Josef
24
2014
Translating higher-order clauses to first-order clauses. Zbl 1203.68188
Meng, Jia; Paulson, Lawrence C.
24
2008
MPTP 0.2: Design, implementation, and initial experiments. Zbl 1113.68095
Urban, Josef
24
2006
Some lambda calculus and type theory formalized. Zbl 0940.03019
McKinna, James; Pollack, Robert
23
1999
An algorithm to evaluate quantified Boolean formulae and its experimental evaluation. Zbl 1002.68165
Cadoli, Marco; Schaerf, Marco; Giovanardi, Andrea; Giovanardi, Massimo
23
2002
Model-theoretic methods in combined constraint satisfiability. Zbl 1069.03008
Ghilardi, Silvio
23
2004
MetiTarski: An automatic theorem prover for real-valued special functions. Zbl 1215.68206
Akbarpour, Behzad; Paulson, Lawrence Charles
23
2010
ATP and presentation service for Mizar formalizations. Zbl 1260.68380
Urban, Josef; Rudnicki, Piotr; Sutcliffe, Geoff
23
2013
lean\(T^ AP\): Lean tableau-based deduction. Zbl 0838.68097
Beckert, Bernhard; Posegga, Joachim
22
1995
Extending Sledgehammer with SMT solvers. Zbl 1314.68272
Blanchette, Jasmin Christian; Böhme, Sascha; Paulson, Lawrence C.
22
2013
Premise selection for mathematics by corpus analysis and kernel methods. Zbl 1315.68217
Alama, Jesse; Heskes, Tom; Kühlwein, Daniel; Tsivtsivadze, Evgeni; Urban, Josef
22
2014
MizAR 40 for Mizar 40. Zbl 1356.68191
Kaliszyk, Cezary; Urban, Josef
22
2015
A logic for reasoning with inconsistency. Zbl 0807.03019
Kifer, Michael; Lozinskii, Eliezer L.
21
1992
Set theory for verification. I: From foundations to functions. Zbl 0802.68128
Paulson, Lawrence C.
21
1993
First-order modal tableaux. Zbl 0648.03004
Fitting, Melvin
21
1988
Non-Horn clause logic programming without contrapositives. Zbl 0666.68091
Plaisted, David A.
21
1988
Backdoor sets of quantified Boolean formulas. Zbl 1191.68353
Samer, Marko; Szeider, Stefan
21
2009
A Skeptic’s approach to combining HOL and Maple. Zbl 0916.68142
Harrison, J.; Théry, L.
20
1998
Branching rules for satisfiability. Zbl 0838.68098
Hooker, J. N.; Vinay, V.
20
1995
Locales: a module system for mathematical theories. Zbl 1315.68218
Ballarin, Clemens
20
2014
Explicit representation of terms defined by counter examples. Zbl 0641.68124
Lassez, J.-L.; Marriott, K.
20
1987
A formally verified compiler back-end. Zbl 1185.68215
Leroy, Xavier
20
2009
MPTP-motivation, implementation, first experiments. Zbl 1075.68081
Urban, Josef
19
2004
Implicit induction in conditional theories. Zbl 0819.68114
Bouhoula, Adel; Rusinowitch, Michaël
18
1995
New worst-case upper bounds for SAT. Zbl 0960.03009
Hirsch, Edward A.
18
2000
Testing positiveness of polynomials. Zbl 0916.68084
Hong, Hoon; Jakuš, Dalibor
18
1998
Experiments with discrimination-tree indexing and path indexing for term retrieval. Zbl 0781.68101
McCune, William
18
1992
Complexity of unification problems with associative-commutative operators. Zbl 0781.68076
Kapur, Deepak; Narendran, Paliath
18
1992
Gentzen-type systems, resolution and tableaux. Zbl 0788.03013
Avron, Arnon
18
1993
Stochastic Boolean satisfiability. Zbl 0988.68189
Littman, Michael L.; Majercik, Stephen M.; Pitassi, Toniann
18
2001
Set theory in first-order logic: Clauses for Gödel’s axioms. Zbl 0635.03008
Boyer, Robert; Lusk, Ewing; McCune, William; Overbeek, Ross; Stickel, Mark E.; Wos, Lawrence
18
1986
From bisimulation to simulation: Coarsest partition problems. Zbl 1081.68052
Gentilini, R.; Piazza, C.; Policriti, A.
17
2003
Ordered semantic hyper-linking. Zbl 0959.68115
Plaisted, David A.; Zhu, Yunshan
17
2000
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
17
2015
Exponential lower bounds for the running time of DPLL algorithms on satisfiable formulas. Zbl 1109.68098
Alekhnovich, Michael; Hirsch, Edward A.; Itsykson, Dmitry
17
2005
On equivalents of well-foundedness. An experiment in MIZAR. Zbl 0944.68168
Rudnicki, Piotr; Trybulec, Andrzej
16
1999
Local search algorithms for SAT: An empirical evaluation. Zbl 0961.68039
Hoos, Holger H.; Stützle, Thomas
16
2000
Positive unit hyperresolution tableaux and their application to minimal model generation. Zbl 0960.03006
Bry, François; Yahya, Adnan
16
2000
A semantical framework for supporting subjective and conditional probabilities in deductive databases. Zbl 0784.68082
Ng, Raymond; Subrahmanian, V. S.
16
1993
Single axioms for groups and abelian groups with various operations. Zbl 0794.20002
McCune, William W.
16
1993
Autarkic computations in formal proofs. Zbl 1002.68156
Barendregt, Henk; Barendsen, Erik
16
2002
Priorities on defaults with prerequisites, and their application in treating specificity in terminological default logic. Zbl 0842.68081
Baader, Franz; Hollunder, Bernhard
16
1995
Proving geometry theorems with rewrite rules. Zbl 0642.68162
Chou, Shang-Ching; Schelter, William F.
16
1986
On the declarative and procedural semantics of logic programs. Zbl 0681.68109
Przymusinski, Teodor C.
16
1989
Weak generalized closed world assumption. Zbl 0683.68086
Rajasekar, Arcot; Lobo, Jorge; Minker, Jack
16
1989
Combining nonstably infinite theories. Zbl 1108.03014
Tinelli, Cesare; Zarba, Calogero G.
16
2005
The area method. A recapitulation. Zbl 1242.68281
Janičić, Predrag; Narboux, Julien; Quaresma, Pedro
16
2012
Hybrid. A definitional two-level approach to reasoning with higher-order abstract syntax. Zbl 1252.68252
Felty, Amy; Momigliano, Alberto
16
2012
A two-level logic approach to reasoning about computations. Zbl 1290.68088
Gacek, Andrew; Miller, Dale; Nadathur, Gopalan
16
2012
Logical cryptanalysis as a SAT problem: Encoding and analysis of the U. S. Data Encryption Standard. Zbl 0968.68052
Massacci, Fabio; Marraro, Laura
15
2000
A deductive database approach to automated geometry theorem proving and discovering. Zbl 0961.68121
Chou, Shang-Ching; Gao, Xiao-Shan; Zhang, Jing-Zhong
15
2000
Reachability analysis over term rewriting systems. Zbl 1075.68038
Feuillade, Guillaume; Genet, Thomas; Viet Triem Tong, Valérie
15
2004
Abstract congruence closure. Zbl 1040.03006
Bachmair, Leo; Tiwari, Ashish; Vigneron, Laurent
15
2003
Data complexity of query answering in expressive description logics via tableaux. Zbl 1154.68102
Ortiz, Magdalena; Calvanese, Diego; Eiter, Thomas
15
2008
Inferring negative information from disjunctive databases. Zbl 0662.68101
Ross, Kenneth A.; Topor, Rodney W.
15
1988
TABLEAUX: A general theorem prover for modal logics. Zbl 0743.03008
Catach, Laurent
15
1991
User interaction with the Matita proof assistant. Zbl 1132.68673
Asperti, Andrea; Sacerdoti Coen, Claudio; Tassi, Enrico; Zacchiroli, Stefano
15
2007
On rewriting rules in Mizar. Zbl 1260.68376
Korniłowicz, Artur
15
2013
Single step tableaux for modal logics. Computational properties, complexity and methodology. Zbl 0951.03008
Massacci, Fabio
14
2000
Implementing the Davis-Putnam method. Zbl 0967.68148
Zhang, Hantao; Stickel, Mark
14
2000
A new approach for automatic theorem proving in real geometry. Zbl 0914.03013
Dolzmann, Andreas; Sturm, Thomas; Weispfenning, Volker
14
1998
Word unification and transformation of generalized equations. Zbl 0802.68136
Schulz, Klaus U.
14
1993
Proof strategies in linear logic. Zbl 0821.03004
Tammet, Tanel
14
1994
The liberalized \(\delta\)-rule in free variable semantic tableaux. Zbl 0826.03005
Hähnle, Reiner; Schmitt, Peter H.
14
1994
A comparison of Mizar and Isar. Zbl 1064.68083
Wenzel, Markus; Wiedijk, Freek
14
2002
Unification in abelian semigroups. Zbl 0637.68106
Herold, Alexander; Siekmann, Jörg H.
14
1987
A more expressive formulation of many sorted logic. Zbl 0642.68166
Cohn, Anthony G.
14
1987
Stable and extension class theory for logic programs and default logics. Zbl 0763.03017
Baral, Chitta R.; Subrahmanian, V. S.
14
1992
A graphical user interface for formal proofs in geometry. Zbl 1131.68094
Narboux, Julien
14
2007
OptiMathSAT: a tool for optimization modulo theories. Zbl 07176604
Sebastiani, Roberto; Trentin, Patrick
2
2020
Strong extension-free proof systems. Zbl 07176609
Heule, Marijn J. H.; Kiesl, Benjamin; Biere, Armin
2
2020
Probably partially true: satisfiability for Łukasiewicz infinitely-valued probabilistic logic and related topics. Zbl 07268902
Finger, Marcelo; Preto, Sandro
2
2020
Using well-founded relations for proving operational termination. Zbl 07176596
Lucas, Salvador
1
2020
Combining induction and saturation-based theorem proving. Zbl 07176598
Echenim, M.; Peltier, N.
1
2020
Solving quantifier-free first-order constraints over finite sets and binary relations. Zbl 07176599
Cristiá, Maximiliano; Rossi, Gianfranco
1
2020
A verified implementation of algebraic numbers in Isabelle/HOL. Zbl 07176602
Joosten, Sebastiaan J. C.; Thiemann, René; Yamada, Akihisa
1
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
1
2020
A verified implementation of the Berlekamp-Zassenhaus factorization algorithm. Zbl 07187044
Divasón, Jose; Joosten, Sebastiaan J. C.; Thiemann, René; Yamada, Akihisa
1
2020
Parallel postulates and continuity axioms: a mechanized study in intuitionistic logic using Coq. Zbl 1441.03011
Boutry, Pierre; Gries, Charly; Narboux, Julien; Schreck, Pascal
5
2019
Verifying OpenJDK’s sort method for generic collections. Zbl 07024053
de Gouw, Stijn; de Boer, Frank S.; Bubel, Richard; Hähnle, Reiner; Rot, Jurriaan; Steinhöfel, Dominic
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
Deciding univariate polynomial problems using untrusted certificates in Isabelle/HOL. Zbl 07024052
Li, Wenda; Passmore, Grant Olney; Paulson, Lawrence C.
2
2019
Fast formal proof of the Erdős-Szekeres conjecture for convex polygons with at most 6 points. Zbl 07038739
Marić, Filip
2
2019
Goal-oriented proof-search in natural deduction for intuitionistic propositional logic. Zbl 07024054
Ferrari, Mauro; Fiorentini, Camillo
1
2019
Proof pearl: Bounding least common multiples with triangles. Zbl 07024455
Chan, Hing-Lun; Norrish, Michael
1
2019
From types to sets by local type definition in higher-order logic. Zbl 07024458
Kunčar, Ondřej; Popescu, Andrei
1
2019
Formalizing network flow algorithms: a refinement approach in Isabelle/HOL. Zbl 07024459
Lammich, Peter; Sefidgar, S. Reza
1
2019
Verifying the correctness and amortized complexity of a union-find implementation in separation logic with time credits. Zbl 07038740
Charguéraud, Arthur; Pottier, François
1
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
1
2019
Refinement to imperative HOL. Zbl 1465.68291
Lammich, Peter
1
2019
A consistent foundation for Isabelle/HOL. Zbl 1465.68289
Kunčar, Ondřej; Popescu, Andrei
1
2019
On the generation of quantified lemmas. Zbl 1459.03011
Ebner, Gabriel; Hetzl, Stefan; Leitsch, Alexander; Reis, Giselle; Weller, Daniel
1
2019
Canonicity for cubical type theory. Zbl 07096713
Huber, Simon
1
2019
Guarded cubical type theory. Zbl 07096714
Birkedal, Lars; Bizjak, Aleš; Clouston, Ranald; Grathwohl, Hans Bugge; Spitters, Bas; Vezzosi, Andrea
1
2019
The James construction and \(\pi _4(\mathbb{S}^{3})\) in homotopy type theory. Zbl 07096715
Brunerie, Guillaume
1
2019
From signatures to monads in UniMath. Zbl 07096716
Ahrens, Benedikt; Matthes, Ralph; Mörtberg, Anders
1
2019
Call-by-value lambda calculus as a model of computation in Coq. Zbl 07096721
Forster, Yannick; Smolka, Gert
1
2019
Reinterpreting dependency schemes: soundness meets incompleteness in DQBF. Zbl 07100457
Beyersdorff, Olaf; Blinkhorn, Joshua; Chew, Leroy; Schmidt, Renate; Suda, Martin
1
2019
Classification of finite fields with applications. Zbl 07100459
Chan, Hing-Lun; Norrish, Michael
1
2019
Formally verifying the solution to the Boolean Pythagorean triples problem. Zbl 07100460
Cruz-Filipe, Luís; Marques-Silva, Joao; Schneider-Kamp, Peter
1
2019
Formalization of metatheory of the Quipper quantum programming language in a linear logic. Zbl 07121996
Mahmoud, Mohamed Yousri; Felty, Amy P.
1
2019
Verifying safety and persistence in hybrid systems using flowpipes and continuous invariants. Zbl 07121998
Sogokon, Andrew; Jackson, Paul B.; Johnson, Taylor T.
1
2019
Compositional falsification of cyber-physical systems with machine learning components. Zbl 07121999
Dreossi, Tommaso; Donzé, Alexandre; Seshia, Sanjit A.
1
2019
Efficient active automata learning via mutation testing. Zbl 07122002
Aichernig, Bernhard K.; Tappler, Martin
1
2019
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
46
2018
Automatic synthesis of logical models for order-sorted first-order theories. Zbl 1398.68095
Lucas, Salvador; Gutiérrez, Raúl
5
2018
Formal verification of an executable LTL model checker with partial order reduction. Zbl 1426.68162
Brunner, Julian; Lammich, Peter
4
2018
Hammer for Coq: automation for dependent type theory. Zbl 1448.68458
Czajka, Łukasz; Kaliszyk, Cezary
4
2018
Synthesis of obfuscation policies to ensure privacy and utility. Zbl 1426.68085
Wu, Yi-Chin; Raman, Vasumathi; Rawlings, Blake C.; Lafortune, Stéphane; Seshia, Sanjit A.
3
2018
A formalization of metric spaces in HOL Light. Zbl 1425.68376
Maggesi, Marco
2
2018
Automated verification of functional correctness of race-free GPU programs. Zbl 1426.68054
Kojima, Kensuke; Imanishi, Akifumi; Igarashi, Atsushi
2
2018
Toward compositional verification of interruptible OS kernels and device drivers. Zbl 1451.68170
Chen, Hao; Wu, Xiongnan; Shao, Zhong; Lockerman, Joshua; Gu, Ronghui
2
2018
Visibly linear temporal logic. Zbl 1425.68182
Bozzelli, Laura; Sánchez, César
1
2018
Bidirectional grammars for machine-code decoding and encoding. Zbl 1426.68069
Tan, Gang; Morrisett, Greg
1
2018
A unifying view on SMT-based software verification. Zbl 1426.68041
Beyer, Dirk; Dangl, Matthias; Wendler, Philipp
1
2018
Sentence-normalized conditional narrowing modulo in rewriting logic and Maude. Zbl 1398.68267
Aguirre, Luis; Martí-Oliet, Narciso; Palomino, Miguel; Pita, Isabel
1
2018
CoSMed: a confidentiality-verified social media platform. Zbl 1451.68168
Bauereiß, Thomas; Pesenti Gritti, Armando; Popescu, Andrei; Raimondi, Franco
1
2018
Verified iptables firewall analysis and verification. Zbl 1451.68173
Diekmann, Cornelius; Hupel, Lars; Michaelis, Julius; Haslbeck, Maximilian; Carle, Georg
1
2018
Mechanising a type-safe model of multithreaded Java with a verified compiler. Zbl 1451.68178
Lochbihler, Andreas
1
2018
A verified SAT solver framework with learn, forget, restart, and incrementality. Zbl 1448.68457
Blanchette, Jasmin Christian; Fleury, Mathias; Lammich, Peter; Weidenbach, Christoph
1
2018
Formalization of the resolution calculus for first-order logic. Zbl 1451.03019
Schlichtkrull, Anders
1
2018
A verified ODE solver and the Lorenz attractor. Zbl 1448.68460
Immler, Fabian
1
2018
A synthetic proof of Pappus’ theorem in Tarski’s geometry. Zbl 1405.03034
Braun, Gabriel; Narboux, Julien
8
2017
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é
8
2017
A fully automatic theorem prover with human-style output. Zbl 1405.03035
Ganesalingam, M.; Gowers, W. T.
6
2017
A formally verified proof of the central limit theorem. Zbl 1425.68369
Avigad, Jeremy; Hölzl, Johannes; Serafin, Luke
5
2017
Combining SAT solvers with computer algebra systems to verify combinatorial conjectures. Zbl 1410.68413
Zulkoski, Edward; Bright, Curtis; Heinle, Albert; Kotsireas, Ilias; Czarnecki, Krzysztof; Ganesh, Vijay
5
2017
Soundness and completeness proofs by coinductive methods. Zbl 1409.68251
Blanchette, Jasmin Christian; Popescu, Andrei; Traytel, Dmitriy
5
2017
Finding proofs in Tarskian geometry. Zbl 1414.68100
Beeson, Michael; Wos, Larry
5
2017
The TPTP problem library and associated infrastructure. From CNF to TH0, TPTP v6.4.0. Zbl 1425.68381
Sutcliffe, Geoff
4
2017
A semantic framework for proof evidence. Zbl 1425.68371
Chihani, Zakaria; Miller, Dale; Renaud, Fabien
4
2017
Automated reducible geometric theorem proving and discovery by Gröbner basis method. Zbl 1425.68383
Zhou, Jie; Wang, Dingkang; Sun, Yao
3
2017
Markov chains and Markov decision processes in Isabelle/HOL. Zbl 1425.68375
Hölzl, Johannes
3
2017
Complexity and resource bound analysis of imperative programs using difference constraints. Zbl 1409.68076
Sinn, Moritz; Zuleger, Florian; Veith, Helmut
3
2017
The OWL reasoner evaluation (ORE) 2015 competition report. Zbl 1425.68402
Parsia, Bijan; Matentzoglu, Nicolas; Gonçalves, Rafael S.; Glimm, Birte; Steigmiller, Andreas
2
2017
Semantically-guided goal-sensitive reasoning: inference system and completeness. Zbl 1437.68189
Bonacina, Maria Paola; Plaisted, David A.
2
2017
A complete uniform substitution calculus for differential dynamic logic. Zbl 1437.03119
Platzer, André
2
2017
On preprocessing techniques and their impact on propositional model counting. Zbl 1409.68259
Lagniez, Jean-Marie; Marquis, Pierre
2
2017
Proving divide and conquer complexities in Isabelle/HOL. Zbl 1414.68101
Eberl, Manuel
2
2017
Higher-order pattern anti-unification in linear time. Zbl 1407.68089
Baumgartner, Alexander; Kutsia, Temur; Levy, Jordi; Villaret, Mateu
2
2017
Automatically proving termination and memory safety for programs with pointer arithmetic. Zbl 1409.68077
Ströder, Thomas; Giesl, Jürgen; Brockschmidt, Marc; Frohn, Florian; Fuhs, Carsten; Hensel, Jera; Schneider-Kamp, Peter; Aschermann, Cornelius
2
2017
Formally proving size optimality of sorting networks. Zbl 1425.68372
Cruz-Filipe, Luís; Larsen, Kim S.; Schneider-Kamp, Peter
1
2017
Preface: Special issue on automatic resource bound analysis. Zbl 1368.00054
Giesl, Jürgen; Hoffmann, Jan
1
2017
Type-based cost analysis for lazy functional languages. Zbl 1409.68067
Jost, Steffen; Vasconcelos, Pedro; Florido, Mário; Hammond, Kevin
1
2017
Lower bounds for runtime complexity of term rewriting. Zbl 1409.68254
Frohn, Florian; Giesl, Jürgen; Hensel, Jera; Aschermann, Cornelius; Ströder, Thomas
1
2017
Abstract interpretation as automated deduction. Zbl 1410.68222
D’Silva, Vijay; Urban, Caterina
1
2017
The Bayesian ontology language \(\mathcal {BEL}\). Zbl 1409.68278
Ceylan, İsmail İlkan; Peñaloza, Rafael
1
2017
Solution validation and extraction for QBF preprocessing. Zbl 1409.68258
Heule, Marijn J. H.; Seidl, Martina; Biere, Armin
1
2017
A learning-based fact selector for Isabelle/HOL. Zbl 1386.68149
Blanchette, Jasmin Christian; Greenaway, David; Kaliszyk, Cezary; Kühlwein, Daniel; Urban, Josef
9
2016
Semi-intelligible Isar proofs from machine-generated proofs. Zbl 1356.68178
Blanchette, Jasmin Christian; Böhme, Sascha; Fleury, Mathias; Smolka, Steffen Juilf; Steckermeier, Albert
8
2016
Adding decision procedures to SMT solvers using axioms with triggers. Zbl 1356.68187
Dross, Claire; Conchon, Sylvain; Kanig, Johannes; Paskevich, Andrei
6
2016
Self-formalisation of higher-order logic. Semantics, soundness, and a verified implementation. Zbl 1356.68194
Kumar, Ramana; Arthan, Rob; Myreen, Magnus O.; Owens, Scott
5
2016
Proving tight bounds on univariate expressions with elementary functions in Coq. Zbl 1386.68151
Martin-Dorel, Érik; Melquiond, Guillaume
4
2016
Psi-calculi in Isabelle. Zbl 1356.68175
Bengtson, Jesper; Parrow, Joachim; Weber, Tjark
4
2016
Semantically-guided goal-sensitive reasoning: model representation. Zbl 1356.68180
Bonacina, Maria Paola; Plaisted, David A.
4
2016
On definitions of constants and types in HOL. Zbl 1356.68173
Arthan, Rob
3
2016
Quasi-decidability of a fragment of the first-order theory of real numbers. Zbl 1437.03047
Franek, Peter; Ratschan, Stefan; Zgliczynski, Piotr
3
2016
Complete instantiation-based interpolation. Zbl 1356.68203
Totla, Nishant; Wies, Thomas
2
2016
Eisbach: a proof method language for Isabelle. Zbl 1356.68195
Matichuk, Daniel; Murray, Toby; Wenzel, Makarius
2
2016
Quantifier reordering for QBF. Zbl 1356.68200
Slivovsky, Friedrich; Szeider, Stefan
2
2016
Formal proofs of rounding error bounds. With application to an automatic positive definiteness check. Zbl 1409.68263
Roux, Pierre
2
2016
Reasoning about algebraic data types with abstractions. Zbl 1386.68104
Pham, Tuan-Hung; Gacek, Andrew; Whalen, Michael W.
1
2016
Automated proofs of block cipher modes of operation. Zbl 1356.68188
Gagné, Martin; Lafourcade, Pascal; Lakhnech, Yassine; Safavi-Naini, Reihaneh
1
2016
Mechanizing a process algebra for network protocols. Zbl 1356.68182
Bourke, Timothy; van Glabbeek, Robert J.; Höfner, Peter
1
2016
A heuristic prover for real inequalities. Zbl 1356.68174
Avigad, Jeremy; Lewis, Robert Y.; Roux, Cody
1
2016
Four decades of {Mizar}. Foreword. Zbl 1336.00111
Grabowski, Adam; Korniłowicz, Artur; Naumowicz, Adam
56
2015
MizAR 40 for Mizar 40. Zbl 1356.68191
Kaliszyk, Cezary; Urban, Josef
22
2015
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
17
2015
The higher-order prover Leo-II. Zbl 1356.68176
Benzmüller, Christoph; Sultana, Nik; Paulson, Lawrence C.; Theiß, Frank
11
2015
...and 629 more Documents
all top 5

Cited by 3,586 Authors

31 Paulson, Lawrence Charles
29 Urban, Josef
27 Eiter, Thomas
25 Meseguer Guaita, José
24 Kaliszyk, Cezary
21 Benzmüller, Christoph Ewald
20 Lucas, Salvador
20 Weidenbach, Christoph
18 Blanchette, Jasmin Christian
18 Gao, Xiaoshan
18 Grabowski, Adam
18 Marques-Silva, João P.
17 Giesl, Jürgen
17 Peltier, Nicolas
17 Voronkov, Andrei
16 Korniłowicz, Artur
16 Middeldorp, Aart
14 Baader, Franz
14 Bonacina, Maria Paola
14 Gottlob, Georg
14 Subramani, Krishnan
14 Tinelli, Cesare
14 Wos, Larry
13 Ayala-Rincón, Mauricio
13 Biere, Armin
13 Bundy, Alan
13 Cantone, Domenico
13 Ghilardi, Silvio
13 Naumowicz, Adam
13 Nipkow, Tobias
13 Schaub, Torsten H.
13 Subrahmanian, V. S.
13 Sutcliffe, Geoff
13 Thiemann, René
12 Calvanese, Diego
12 Kohlhase, Michael
12 Pąk, Karol
12 Plaisted, David Alan
12 Rusinowitch, Michaël
12 Schneider-Kamp, Peter
12 Szeider, Stefan
12 Waldmann, Uwe
11 Baumgartner, Peter
11 Bonatti, Piero Andrea
11 Giunchiglia, Enrico
11 Janičić, Predrag
11 Kapur, Deepak
11 Koch, Sebastian
11 Narboux, Julien
11 Rabe, Florian
11 Smolka, Gert
11 Tahar, Sofiène
11 Wang, Dongming
10 Alviano, Mario
10 Avron, Arnon
10 Botana, Francisco
10 Kirchner, Claude
10 Kovács, Zoltán
10 Leone, Nicola
10 Maratea, Marco
10 Miller, Dale Allen
10 Montanari, Angelo
10 Platzer, André
10 Zhang, Hantao
9 Amgoud, Leila
9 Armando, Alessandro
9 Chou, Shangching
9 Echenim, Mnacho
9 Egly, Uwe
9 Felty, Amy P.
9 Gabbay, Dov M.
9 Gabbay, Murdoch James
9 Hasan, Osman
9 Horrocks, Ian
9 Kerber, Manfred
9 Kinyon, Michael K.
9 Kutsia, Temur
9 Lutz, Carsten
9 McCune, William W.
9 Nakasho, Kazuhisa
9 Narendran, Paliath
9 Nigam, Vivek
9 Omodeo, Eugenio Giovanni
9 Peñaloza, Rafael
9 Pientka, Brigitte
9 Ranise, Silvio
9 Recio, Tomas
9 Ringeissen, Christophe
9 Schmidt-Schauß, Manfred
9 Shidama, Yasunari
9 Szałas, Andrzej
9 Veroff, Robert
9 Wolter, Frank
9 Zakharyaschev, Michael Viktorovich
8 Albert, Elvira
8 Böhme, Sascha
8 Dixon, Clare
8 Dowek, Gilles
8 Farmer, William M.
8 Fernández, Maribel
...and 3,486 more Authors
all top 5

Cited in 201 Journals

445 Journal of Automated Reasoning
184 Artificial Intelligence
180 Theoretical Computer Science
123 Journal of Symbolic Computation
119 Annals of Mathematics and Artificial Intelligence
77 Information and Computation
77 Formalized Mathematics
59 Theory and Practice of Logic Programming
45 Formal Aspects of Computing
44 MSCS. Mathematical Structures in Computer Science
43 Journal of Applied Logic
39 International Journal of Approximate Reasoning
37 Journal of Applied Non-Classical Logics
32 Annals of Pure and Applied Logic
30 Discrete Applied Mathematics
29 Journal of Logical and Algebraic Methods in Programming
26 Formal Methods in System Design
26 Logical Methods in Computer Science
25 Information Processing Letters
25 Mathematics in Computer Science
23 Journal of Functional Programming
23 Constraints
21 Information Sciences
21 Journal of Computer and System Sciences
20 Fuzzy Sets and Systems
19 Studia Logica
18 ACM Transactions on Computational Logic
17 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
11 The Journal of Logic and Algebraic Programming
11 Logica Universalis
10 The Journal of Symbolic Logic
10 Journal of Computer Science and Technology
8 Science of Computer Programming
8 International Journal of Computer Mathematics
7 Journal of Philosophical Logic
7 Notre Dame Journal of Formal Logic
7 AI Communications
7 JETAI. Journal of Experimental & Theoretical Artificial Intelligence
7 Computational Geometry
7 Journal of Logic, Language and Information
7 The Bulletin of Symbolic Logic
6 International Journal of General Systems
6 Mathematics and Computers in Simulation
6 Synthese
6 Computers & Operations Research
6 European Journal of Operational Research
6 Fundamenta Informaticae
6 Computer Languages, Systems & Structures
6 Prikladnaya Diskretnaya Matematika
5 International Journal of Intelligent Systems
5 Annals of Operations Research
5 Soft Computing
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
4 Communications in Algebra
4 Algorithmica
4 Mathematical and Computer Modelling
4 Indagationes Mathematicae. New Series
4 Computational Complexity
4 Journal of Mathematical Sciences (New York)
4 Theory of Computing Systems
4 LMS Journal of Computation and Mathematics
4 International Journal of Applied Mathematics and Computer Science
4 Journal of Applied Mathematics
4 The Review of Symbolic Logic
4 Revista de la Real Academia de Ciencias Exactas, Físicas y Naturales. Serie A: Matemáticas. RACSAM
3 Automatica
3 Journal of Algebra
3 Semigroup Forum
3 Machine Learning
3 International Journal of Foundations of Computer Science
3 Archive for Mathematical Logic
3 Cybernetics and Systems Analysis
3 Journal of Heuristics
3 Mathematical Problems in Engineering
3 RAIRO. Theoretical Informatics and Applications
3 Journal of Discrete Algorithms
3 Nonlinear Analysis. Hybrid Systems
2 Discrete Mathematics
2 Mathematics of Computation
2 The Mathematical Intelligencer
2 Journal of Mathematical Economics
2 Programming and Computer Software
2 Results in Mathematics
2 Transactions of the American Mathematical Society
2 History and Philosophy of Logic
2 Order
2 Journal of Cryptology
2 Science in China. Series A
2 Pattern Recognition
2 Mathematical Logic Quarterly (MLQ)
2 The Journal of Artificial Intelligence Research (JAIR)
2 Journal of Combinatorial Optimization
2 International Journal of Uncertainty, Fuzziness and Knowledge-Based Systems
...and 101 more Journals
all top 5

Cited in 51 Fields

2,643 Computer science (68-XX)
1,086 Mathematical logic and foundations (03-XX)
98 Operations research, mathematical programming (90-XX)
78 Information and communication theory, circuits (94-XX)
59 Geometry (51-XX)
57 Numerical analysis (65-XX)
51 Combinatorics (05-XX)
42 Commutative algebra (13-XX)
40 Number theory (11-XX)
39 Order, lattices, ordered algebraic structures (06-XX)
38 Game theory, economics, finance, and other social and behavioral sciences (91-XX)
34 Group theory and generalizations (20-XX)
27 Field theory and polynomials (12-XX)
22 General and overarching topics; collections (00-XX)
22 Algebraic geometry (14-XX)
22 Category theory; homological algebra (18-XX)
22 Systems theory; control (93-XX)
20 History and biography (01-XX)
20 Real functions (26-XX)
18 General algebraic systems (08-XX)
13 Ordinary differential equations (34-XX)
13 Algebraic topology (55-XX)
11 Statistics (62-XX)
11 Biology and other natural sciences (92-XX)
10 Linear and multilinear algebra; matrix theory (15-XX)
10 Probability theory and stochastic processes (60-XX)
10 Mathematics education (97-XX)
9 Associative rings and algebras (16-XX)
8 Dynamical systems and ergodic theory (37-XX)
8 Operator theory (47-XX)
7 Measure and integration (28-XX)
7 Partial differential equations (35-XX)
6 Special functions (33-XX)
6 Convex and discrete geometry (52-XX)
6 Mechanics of particles and systems (70-XX)
5 Quantum theory (81-XX)
3 Nonassociative rings and algebras (17-XX)
3 Approximations and expansions (41-XX)
3 Harmonic analysis on Euclidean spaces (42-XX)
3 Differential geometry (53-XX)
3 Optics, electromagnetic theory (78-XX)
2 Difference and functional equations (39-XX)
2 Integral equations (45-XX)
2 Calculus of variations and optimal control; optimization (49-XX)
2 General topology (54-XX)
2 Fluid mechanics (76-XX)
1 Functions of a complex variable (30-XX)
1 Several complex variables and analytic spaces (32-XX)
1 Sequences, series, summability (40-XX)
1 Functional analysis (46-XX)
1 Mechanics of deformable solids (74-XX)

Citations by Year