Found 255 Documents (Results 1–100)
Reductive logic, proof-search, and coalgebra: a perspective from resource semantics. (English) Zbl 07920696
Palmigiano, Alessandra (ed.) et al., Samson Abramsky on logic and structure in computer science and beyond. Cham: Springer. Outst. Contrib. Log. 25, 833-875 (2023).
Solving constrained Horn clauses over algebraic data types. (English) Zbl 1529.68167
Dragoi, Cezara (ed.) et al., Verification, model checking, and abstract interpretation. 24th international conference, VMCAI 2023, Boston, MA, USA, January 16–17, 2023. Proceedings. Cham: Springer. Lect. Notes Comput. Sci. 13881, 341-365 (2023).
Synthetic undecidability and incompleteness of first-order axiom systems in Coq. Extended version. (English) Zbl 07695716
MSC:
68V15
Analysis and transformation of constrained Horn clauses for program verification. (English) Zbl 1541.68215
Getting saturated with induction. (English) Zbl 1528.68391
Raskin, Jean-François (ed.) et al., Principles of systems design. Essays dedicated to Thomas A. Henzinger on the occasion of his 60th birthday. Cham: Springer. Lect. Notes Comput. Sci. 13660, 306-322 (2022).
Definitional quantifiers realise semantic reasoning for proof by induction. (English) Zbl 1514.68311
Kovács, Laura (ed.) et al., Tests and proofs. 16th international conference, TAP 2022, held as part of STAF 2022, Nantes, France, July 5, 2022. Proceedings. Cham: Springer. Lect. Notes Comput. Sci. 13361, 48-66 (2022).
MSC:
68V15
A probabilistic approximate logic for neuro-symbolic learning and reasoning. (English) Zbl 1523.68095
Symbolic automatic relations and their applications to SMT and CHC solving. (English) Zbl 1497.68320
Drăgoi, Cezara (ed.) et al., Static analysis. 28th international symposium, SAS 2021, Chicago, IL, USA, October 17–19, 2021. Proceedings. Cham: Springer. Lect. Notes Comput. Sci. 12913, 405-428 (2021).
Towards finding longer proofs. (English) Zbl 07532515
Das, Anupam (ed.) et al., Automated reasoning with analytic tableaux and related methods. 30th international conference, TABLEAUX 2021, Birmingham, UK, September 6–9, 2021. Proceedings. Cham: Springer. Lect. Notes Comput. Sci. 12842, 167-186 (2021).
MSC:
68V15
AlCons: deductive synthesis of sorting algorithms in Theorema. (English) Zbl 07500651
Cerone, Antonio (ed.) et al., Theoretical aspects of computing – ICTAC 2021. 18th international colloquium, virtual event, Nur-Sultan, Kazakhstan, September 8–10, 2021. Proceedings. Cham: Springer. Lect. Notes Comput. Sci. 12819, 314-333 (2021).
MSC:
68Qxx
Theory exploration powered by deductive synthesis. (English) Zbl 1493.68388
Silva, Alexandra (ed.) et al., Computer aided verification. 33rd international conference, CAV 2021, virtual event, July 20–23, 2021. Proceedings. Part II. Cham: Springer. Lect. Notes Comput. Sci. 12760, 125-148 (2021).
Distilling the requirements of Gödel’s incompleteness theorems with a proof assistant. (English) Zbl 1543.03082
Metrically homogeneous graphs of diameter \(3\). (English) Zbl 1490.03020
Reviewer: Vera Koponen (Uppsala)
Removing algebraic data types from constrained Horn clauses using difference predicates. (English) Zbl 07614508
Peltier, Nicolas (ed.) et al., Automated reasoning. 10th international joint conference, IJCAR 2020, Paris, France, July 1–4, 2020. Proceedings. Part I. Cham: Springer. Lect. Notes Comput. Sci. 12166, 83-102 (2020).
MSC:
68V15
Transformational verification of Quicksort. (English) Zbl 07453193
Fribourg, Laurent (ed.) et al., Proceedings of the eighth international workshop on verification and program transformation and the seventh workshop on Horn clauses for verification and synthesis, VPT/HCVS 2020, Dublin, Ireland, April 25–26, 2020. Waterloo: Open Publishing Association (OPA). Electron. Proc. Theor. Comput. Sci. (EPTCS) 320, 95-109 (2020).
Automated detection of interesting properties in regular polygons. (English) Zbl 1466.51009
Reviewer: Cătălin Barbu (Bačau)
Conflict generalisation in ASP: learning correct and effective non-ground constraints. (English) Zbl 1468.68174
Proving properties of sorting programs: a case study in Horn clause verification. (English) Zbl 1483.68189
De Angelis, Emanuele (ed.) et al., Proceedings of the sixth workshop on Horn clauses for verification and synthesis, HCVS 2019, and the third workshop on program equivalence and relational reasoning, PERR 2019, Prague, Czech Republic, April 6–7, 2019. Waterloo: Open Publishing Association (OPA). Electron. Proc. Theor. Comput. Sci. (EPTCS) 296, 48-75 (2019).
A formally verified abstract account of Gödel’s incompleteness theorems. (English) Zbl 1535.03284
Fontaine, Pascal (ed.), Automated deduction – CADE 27. 27th international conference on automated deduction, Natal, Brazil, August 27–30, 2019. Proceedings. Cham: Springer. Lect. Notes Comput. Sci. 11716, 442-461 (2019).
Confluence by critical pair analysis revisited. (English) Zbl 1535.68122
Fontaine, Pascal (ed.), Automated deduction – CADE 27. 27th international conference on automated deduction, Natal, Brazil, August 27–30, 2019. Proceedings. Cham: Springer. Lect. Notes Comput. Sci. 11716, 319-336 (2019).
MSC:
68Q42
Discussing Hilbert’s 24th problem. (English) Zbl 1441.03006
Philos. Trans. R. Soc. Lond., A, Math. Phys. Eng. Sci. 377, No. 2140, Article ID 20180040, 10 p. (2019).
Reviewer: Victor V. Pambuccian (Glendale)
Automated mutual induction proof in separation logic. (English) Zbl 1425.68382
MSC:
68T15
03B70
Mechanical synthesis of sorting algorithms for binary trees by logic and combinatorial techniques. (English) Zbl 1395.68246
MSC:
68T15
68P10
Discovering geometry theorems in regular polygons. (English) Zbl 1515.68345
Fleuriot, Jacques (ed.) et al., Artificial intelligence and symbolic computation. 13th international conference, AISC 2018, Suzhou, China, September 16–19, 2018. Proceedings. Cham: Springer. Lect. Notes Comput. Sci. 11110, 155-169 (2018).
Machine learning for inductive theorem proving. (English) Zbl 1515.68344
Fleuriot, Jacques (ed.) et al., Artificial intelligence and symbolic computation. 13th international conference, AISC 2018, Suzhou, China, September 16–19, 2018. Proceedings. Cham: Springer. Lect. Notes Comput. Sci. 11110, 87-103 (2018).
Into the infinite – theory exploration for coinduction. (English) Zbl 1515.68343
Fleuriot, Jacques (ed.) et al., Artificial intelligence and symbolic computation. 13th international conference, AISC 2018, Suzhou, China, September 16–19, 2018. Proceedings. Cham: Springer. Lect. Notes Comput. Sci. 11110, 70-86 (2018).
Investigating diagrammatic reasoning with deep neural networks. (English) Zbl 1508.68313
Chapman, Peter (ed.) et al., Diagrammatic representation and inference. 10th international conference, Diagrams 2018, Edinburgh, UK, June 18–22, 2018. Proceedings. Cham: Springer. Lect. Notes Comput. Sci. 10871, 390-398 (2018).
Can an A.I. win a medal in the mathematical olympiad? – Benchmarking mechanized mathematics on pre-university problems. (English) Zbl 1462.68152
Mathematical inference and logical inference. (English) Zbl 1434.00030
Reviewer: Roman Murawski (Poznań)
MSC:
00A30
Equivalence checking of two functional programs using inductive theorem provers. (English) Zbl 1419.68038
MSC:
68N18
68T15
Mathematical logic: proof theory, constructive mathematics. Abstracts from the workshop held November 5–11, 2017. (English) Zbl 1409.00077
A new compact finite difference quasilinearization method for nonlinear evolution partial differential equations. (English) Zbl 1382.65240
Automated theory exploration for interactive theorem proving: an introduction to the Hipster system. (English) Zbl 1483.68484
Ayala-Rincón, Mauricio (ed.) et al., Interactive theorem proving. 8th international conference, ITP 2017, Brasília, Brazil, September 26–29, 2017. Proceedings. Cham: Springer. Lect. Notes Comput. Sci. 10499, 1-11 (2017).
MSC:
68V15
Quick specifications for the busy programmer. (English) Zbl 1418.68037
MSC:
68N18
Lakatos-style collaborative mathematics through dialectical, structured and abstract argumentation. (English) Zbl 1419.68127
The natural algorithmic approach of mixed trigonometric-polynomial problems. (English) Zbl 1373.42003
Proof mining with dependent types. (English) Zbl 1367.68251
Geuvers, Herman (ed.) et al., Intelligent computer mathematics. 10th international conference, CICM 2017, Edinburgh, UK, July 17–21, 2017. Proceedings. Cham: Springer (ISBN 978-3-319-62074-9/pbk; 978-3-319-62075-6/ebook). Lecture Notes in Computer Science 10383. Lecture Notes in Artificial Intelligence, 303-318 (2017).
MSC:
68T15
68T05
A fully automatic theorem prover with human-style output. (English) Zbl 1405.03035
MSC:
03B35
68T15
Understanding and maintaining tactics graphically OR how we are learning that a diagram can be worth more than 10K LoC. (English) Zbl 1451.68324
Enhancing unsatisfiable cores for LTL with information on temporal relevance. (English) Zbl 1356.68146
Schematic cut elimination and the ordered pigeonhole principle. (English) Zbl 1476.03079
Olivetti, Nicola (ed.) et al., Automated reasoning. 8th international joint conference, IJCAR 2016, Coimbra, Portugal, June 27 – July 2, 2016. Proceedings. Cham: Springer. Lect. Notes Comput. Sci. 9706, 241-256 (2016).
Model finding for recursive functions in SMT. (English) Zbl 1475.68448
Olivetti, Nicola (ed.) et al., Automated reasoning. 8th international joint conference, IJCAR 2016, Coimbra, Portugal, June 27 – July 2, 2016. Proceedings. Cham: Springer. Lect. Notes Comput. Sci. 9706, 133-151 (2016).
Automated conjecturing. I: Fajtlowicz’s Dalmatian heuristic revisited. (English) Zbl 1344.68208
MSC:
68T15
68T20
A deflationary account of the truth of the Gödel sentence \(\mathcal{G}\). (English) Zbl 1429.03041
Lolli, Gabriele (ed.) et al., From logic to practice. Italian studies in the philosophy of mathematics. Cham: Springer. Boston Stud. Philos. Hist. Sci. 308, 71-90 (2015).
Flexary connectives in Mizar. (English) Zbl 1387.68207
MSC:
68T15
03B35
Invited talk: On a (quite) universal theorem proving approach and its application in metaphysics. (English) Zbl 1471.68302
De Nivelle, Hans (ed.), Automated reasoning with analytic tableaux and related methods. 24th international conference, TABLEAUX 2015, Wrocław, Poland, September 21–24, 2015. Proceedings. Cham: Springer. Lect. Notes Comput. Sci. 9323, 213-220 (2015).
Quantomatic: a proof assistant for diagrammatic reasoning. (English) Zbl 1465.68288
Felty, Amy P. (ed.) et al., Automated deduction – CADE-25. 25th international conference on automated deduction, Berlin, Germany, August 1–7, 2015. Proceedings. Cham: Springer. Lect. Notes Comput. Sci. 9195, 326-336 (2015).
TIP: tons of inductive problems. (English) Zbl 1417.68179
Kerber, Manfred (ed.) et al., Intelligent computer mathematics. International conference, CICM 2015, Washington, DC, USA, July 13–17, 2015, Proceedings. Cham: Springer. Lect. Notes Comput. Sci. 9150, 333-337 (2015).
MSC:
68T15
ASP, amalgamation, and the conceptual blending workflow. (English) Zbl 1467.68165
Calimeri, Francesco (ed.) et al., Logic programming and nonmonotonic reasoning. 13th international conference, LPNMR 2015, Lexington, KY, USA, September 27–30, 2015. Proceedings. Cham: Springer. Lect. Notes Comput. Sci. 9345, 309-316 (2015).
Analogy in automated deduction: a survey. (English) Zbl 1341.68183
Prade, Henri (ed.) et al., Computational approaches to analogical reasoning: current trends. Revised and extended versions of papers based on the presentations at the international workshop on similarity and analogy-based methods in AI, SAMAI ’12, co-located with the 20th European conference on artificial intelligence, ECAI ’12, Montpellier, France, August 27, 2012. Berlin: Springer (ISBN 978-3-642-54515-3/hbk; 978-3-642-54516-0/ebook). Studies in Computational Intelligence 548, 103-130 (2014).
MSC:
68T15
03B35
Modeling ontology evolution with SetPi. (English) Zbl 1320.68175
MSC:
68T30
Recycling proof patterns in Coq: case studies. (English) Zbl 1302.68243
MSC:
68T15
68T05
Algorithmic introduction of quantified cuts. (English) Zbl 1393.03050
MSC:
03F05
Mining state-based models from proof corpora. (English) Zbl 1304.68155
Watt, Stephen M. (ed.) et al., Intelligent computer mathematics. International conference, CICM 2014, Coimbra, Portugal, July 7–11, 2014. Proceedings. Berlin: Springer (ISBN 978-3-319-08433-6/pbk). Lecture Notes in Computer Science 8543. Lecture Notes in Artificial Intelligence, 282-297 (2014).
MSC:
68T15
Hipster: integrating theory exploration in a proof assistant. (English) Zbl 1304.68157
Watt, Stephen M. (ed.) et al., Intelligent computer mathematics. International conference, CICM 2014, Coimbra, Portugal, July 7–11, 2014. Proceedings. Berlin: Springer (ISBN 978-3-319-08433-6/pbk). Lecture Notes in Computer Science 8543. Lecture Notes in Artificial Intelligence, 108-122 (2014).
MSC:
68T15
Ours is to reason why. (English) Zbl 1390.68186
Liu, Zhiming (ed.) et al., Theories of programming and formal methods. Essays dedicated to Jifeng He on the occasion of his 70th birthday. Berlin: Springer (ISBN 978-3-642-39697-7/pbk). Lecture Notes in Computer Science 8051, 227-243 (2013).
MSC:
68N30
Narrowing based inductive proof search. (English) Zbl 1383.03019
Voronkov, Andrei (ed.) et al., Programming logics. Essays in memory of Harald Ganzinger. Berlin: Springer (ISBN 978-3-642-37650-4/pbk). Lecture Notes in Computer Science 7797, 216-238 (2013).
Automating induction with an SMT solver. (English) Zbl 1326.68262
Kuncak, Viktor (ed.) et al., Verification, model checking, and abstract interpretation. 13th international conference, VMCAI 2012, Philadelphia, PA, USA, January 22–24, 2012. Proceedings. Berlin: Springer (ISBN 978-3-642-27939-3/pbk). Lecture Notes in Computer Science 7148, 315-331 (2012).
Proving properties about functions on lists involving element tests. (English) Zbl 1312.68076
Mossakowski, Till (ed.) et al., Recent trends in algebraic development techniques. 20th international workshop, WADT 2010, Etelsen, Germany, July 1–4, 2010. Revised selected papers. Berlin: Springer (ISBN 978-3-642-28411-3/pbk). Lecture Notes in Computer Science 7137, 270-286 (2012).
Conjecture synthesis for inductive theories. (English) Zbl 1243.68268
MSC:
68T15
Proving termination by dependency pairs and inductive theorem proving. (English) Zbl 1243.68267
MSC:
68T15
68Q42
Automated theorem provers: a practical tool for the working mathematician? (English) Zbl 1237.68177
Reviewer: G. E. Mints (Stanford)
MSC:
68T15
Heterogeneous proofs: spider diagrams meet higher-order provers. (English) Zbl 1342.68305
Van Eekelen, Marko (ed.) et al., Interactive theorem proving. Second international conference, ITP 2011, Berg en Dal, The Netherlands, August 22–25, 2011. Proceedings. Berlin: Springer (ISBN 978-3-642-22862-9/pbk). Lecture Notes in Computer Science 6898, 376-382 (2011).
MSC:
68T15
Interleaving strategies. (English) Zbl 1335.68290
Davenport, James H. (ed.) et al., Intelligent computer mathematics. 18th symposium, Calculemus 2011, and 10th international conference, MKM 2011, Bertinoro, Italy, July 18–23, 2011. Proceedings. Berlin: Springer (ISBN 978-3-642-22672-4/pbk). Lecture Notes in Computer Science 6824. Lecture Notes in Artificial Intelligence, 196-211 (2011).
Using Theorema in the formalization of theoretical economics. (English) Zbl 1335.68231
Davenport, James H. (ed.) et al., Intelligent computer mathematics. 18th symposium, Calculemus 2011, and 10th international conference, MKM 2011, Bertinoro, Italy, July 18–23, 2011. Proceedings. Berlin: Springer (ISBN 978-3-642-22672-4/pbk). Lecture Notes in Computer Science 6824. Lecture Notes in Artificial Intelligence, 58-73 (2011).
MSC:
68T15
91-04
Automated cyclic entailment proofs in separation logic. (English) Zbl 1341.68184
Bjørner, Nikolaj (ed.) et al., Automated deduction – CADE-23. 23rd international conference on automated deduction, Wrocław, Poland, July 31 – August 5, 2011. Proceedings. Berlin: Springer (ISBN 978-3-642-22437-9/pbk; 978-3-642-22438-6/ebook). Lecture Notes in Computer Science 6803. Lecture Notes in Artificial Intelligence, 131-146 (2011).
MSC:
68T15
03B70
The use of embeddings to provide a clean separation of term and annotation for higher order rippling. (English) Zbl 1216.68232
MSC:
68T15
Reasoning about assignments in recursive data structures. (English) Zbl 1325.68157
Davies, Jim (ed.) et al., Formal methods: foundations and applications. 13th Brazilian symposium on formal methods, SBMF 2010, Natal, Brazil, November 8–11, 2010. Revised selected papers. Berlin: Springer (ISBN 978-3-642-19828-1/pbk). Lecture Notes in Computer Science 6527, 161-176 (2011).
Efficient on-line algorithms for Euler diagram region computation. (English) Zbl 1200.65015
MSC:
65D18
Visually dynamic presentation of proofs in plane geometry. I: Basic features and the manual input method. (English) Zbl 1211.68372
Dynamic rippling, middle-out reasoning and lemma discovery. (English) Zbl 1309.68169
Siegler, Simon (ed.) et al., Verification, induction, termination analysis. Festschrift for Christoph Walther on the occasion of his 60th birthday. Berlin: Springer (ISBN 978-3-642-17171-0/pbk). Lecture Notes in Computer Science 6463. Lecture Notes in Artificial Intelligence, 102-116 (2010).
MSC:
68T15
Perfect discrimination graphs: indexing terms with integer exponents. (English) Zbl 1291.68324
Giesl, Jürgen (ed.) et al., Automated reasoning. 5th international joint conference, IJCAR 2010, Edinburgh, UK, July 16–19, 2010. Proceedings. Berlin: Springer (ISBN 978-3-642-14202-4/pbk). Lecture Notes in Computer Science 6173. Lecture Notes in Artificial Intelligence, 369-383 (2010).
MSC:
68T15
A single-significant-digit calculus for semi-automated guesstimation. (English) Zbl 1291.68315
Giesl, Jürgen (ed.) et al., Automated reasoning. 5th international joint conference, IJCAR 2010, Edinburgh, UK, July 16–19, 2010. Proceedings. Berlin: Springer (ISBN 978-3-642-14202-4/pbk). Lecture Notes in Computer Science 6173. Lecture Notes in Artificial Intelligence, 354-368 (2010).
MSC:
68T15
A decidable class of nested iterated schemata. (English) Zbl 1291.03014
Giesl, Jürgen (ed.) et al., Automated reasoning. 5th international joint conference, IJCAR 2010, Edinburgh, UK, July 16–19, 2010. Proceedings. Berlin: Springer (ISBN 978-3-642-14202-4/pbk). Lecture Notes in Computer Science 6173. Lecture Notes in Artificial Intelligence, 293-308 (2010).
Crystal: Integrating structured queries into a tactic language. (English) Zbl 1185.68618
MSC:
68T15
68N15
Automating soundness proofs. (English) Zbl 1339.68160
Hennessy, Matthew (ed.) et al., Proceedings of the 5th workshop on structural operational semantics (SOS 2008), Reykjavik, Iceland, July 6, 2008. Amsterdam: Elsevier. Electronic Notes in Theoretical Computer Science 229, No. 4, 107-118 (2009).
Filter Results by …
Document Type
- Journal Articles (165)
- Collection Articles (90)
all
top 5
Author
- Bundy, Alan (23)
- Hutter, Dieter (7)
- Johansson, Moa (7)
- Smaill, Alan (6)
- Giesl, Jürgen (5)
- Hetzl, Stefan (5)
- Ireland, Andrew (5)
- Jamnik, Mateja (5)
- Jebelean, Tudor (5)
- Melis, Erica (5)
- Basin, David A. (4)
- De Angelis, Emanuele (4)
- Dixon, Lucas (4)
- Drămnesc, Isabela (4)
- Fioravanti, Fabio (4)
- Green, Ian (4)
- Leitsch, Alexander (4)
- Peltier, Nicolas (4)
- Proietti, Maurizio (4)
- Siekmann, Jörg H. (4)
- Walsh, Toby (4)
- Benzmüller, Christoph Ewald (3)
- Claessen, Koen (3)
- Fuhs, Carsten (3)
- Kerber, Manfred (3)
- Kolbe, Thomas H. (3)
- Liu, Weiru (3)
- Maclean, Ewen (3)
- Pettorossi, Alberto (3)
- Pym, David J. (3)
- Smallbone, Nicholas (3)
- Stapleton, Gem (3)
- Stratulat, Sorin (3)
- van Harmelen, Frank (3)
- Walther, Christoph (3)
- Yao, Yiyu (3)
- Autexier, Serge (2)
- Bronsard, Francois (2)
- Caferra, Ricardo (2)
- Carette, Jacques (2)
- Colton, Simon (2)
- Confalonieri, Roberto (2)
- Demba, Moussa (2)
- Dennis, Louise Abigail (2)
- Eppe, Manfred (2)
- Farmer, William M. (2)
- Fish, Andrew (2)
- Fleuriot, Jacques D. (2)
- Friedrich, Gerhard E. (2)
- Gheorghiu, Alexander V. (2)
- Ghilardi, Silvio (2)
- Giunchiglia, Fausto (2)
- Grov, Gudmund (2)
- Hamami, Yacin (2)
- Hasker, Robert W. (2)
- Heeren, Bastiaan (2)
- Heras, Jónathan (2)
- Hesketh, Jane (2)
- Huang, Xiaorong (2)
- Jeuring, Johan (2)
- Kaliszyk, Cezary (2)
- Kohlhase, Michael (2)
- Komendantskaya, Ekaterina (2)
- Kounalis, Emmanuel (2)
- Kovács, Laura Ildikó (2)
- Kraan, Ina (2)
- Kramosil, Ivan (2)
- Kraus, Sarit (2)
- Kulpa, Zenon (2)
- Kutz, Oliver (2)
- Lin, Yuhui (2)
- Lisitsa, Alexei P. (2)
- Mantel, Heiko (2)
- Meier, Andreas (2)
- Paris, Jeffrey Bruce (2)
- Parting, Michael (2)
- Plaza, Enric (2)
- Popescu, Andrei (2)
- Protzen, Martin (2)
- Reddy, Uday S. (2)
- Reis, Giselle (2)
- Rosen, Dan (2)
- Schairer, Axel (2)
- Schneider-Kamp, Peter (2)
- Schorlemmer, Marco (2)
- Sengler, Claus (2)
- Swiderski, Stephan (2)
- Traytel, Dmitry (2)
- Urban, Josef (2)
- Urbas, Matej (2)
- Vierling, Jannik (2)
- Voigtlander, Janis (2)
- Wang, Lusheng (2)
- Weller, Daniel S. (2)
- Windsteiger, Wolfgang (2)
- Wong, S. K. Michael (2)
- Abourbih, Jonathan A. (1)
- Adams, Andrew A. (1)
- Algehed, Maximilian (1)
- Åman Pohjola, Johannes (1)
- and 321 more Authors
all
top 5
Serial
- J. Autom. Reasoning (33)
- Artif. Intell. (31)
- Theor. Comput. Sci. (7)
- J. Symb. Comput. (7)
- Ann. Math. Artif. Intell. (7)
- Int. J. Approx. Reasoning (5)
- J. Appl. Log. (5)
- Inf. Sci. (4)
- Formal Asp. Comput. (4)
- Int. J. Gen. Syst. (3)
- Ann. Pure Appl. Logic (3)
- Int. J. Intell. Syst. (3)
- Form. Methods Syst. Des. (3)
- Math. Comput. Sci. (3)
- Arch. Math. Logic (2)
- Philos. Trans. R. Soc. Lond., Ser. A, Math. Phys. Eng. Sci. (2)
- J. Log. Algebr. Program. (2)
- Theory Pract. Log. Program. (2)
- Rev. Symb. Log. (2)
- J. Log. Algebr. Methods Program. (2)
- Comput. Math. Appl. (1)
- Inf. Process. Lett. (1)
- Lett. Math. Phys. (1)
- Theor. Comput. Fluid Dyn. (1)
- Appl. Math. Comput. (1)
- Kybernetika (1)
- Program. Comput. Softw. (1)
- Stud. Log. (1)
- Synthese (1)
- J. Comput. Sci. Technol. (1)
- Inf. Comput. (1)
- Appl. Math. Lett. (1)
- AI Commun. (1)
- Mach. Learn. (1)
- J. Exp. Theor. Artif. Intell. (1)
- Neural Comput. (1)
- Comput. Geom. (1)
- Linear Algebra Appl. (1)
- J. Logic Lang. Inf. (1)
- J. Appl. Non-Class. Log. (1)
- J. Funct. Program. (1)
- J. Artif. Intell. Res. (JAIR) (1)
- J. Inequal. Appl. (1)
- LMS J. Comput. Math. (1)
- Found. Sci. (1)
- J. Math. Log. (1)
- Int. J. Uncertain. Fuzziness Knowl.-Based Syst. (1)
- Comput. Lang. Syst. Struct. (1)
- ACM Trans. Comput. Log. (1)
- Oberwolfach Rep. (1)
- Log. Univers. (1)
- J. Formaliz. Reason. (1)
- Open Math. (1)
- Philos. Trans. R. Soc. Lond., A, Math. Phys. Eng. Sci. (1)
all
top 5
Year of Publication
- 2024 (1)
- 2023 (5)
- 2022 (8)
- 2021 (9)
- 2020 (5)
- 2019 (8)
- 2018 (10)
- 2017 (9)
- 2016 (5)
- 2015 (11)
- 2014 (6)
- 2013 (2)
- 2012 (3)
- 2011 (10)
- 2010 (7)
- 2009 (10)
- 2008 (7)
- 2007 (9)
- 2006 (11)
- 2005 (9)
- 2004 (7)
- 2003 (4)
- 2002 (2)
- 2001 (5)
- 2000 (5)
- 1999 (1)
- 1998 (3)
- 1997 (5)
- 1996 (23)
- 1995 (5)
- 1994 (16)
- 1993 (7)
- 1992 (3)
- 1991 (6)
- 1990 (7)
- 1989 (5)
- 1988 (1)
- 1987 (2)
- 1986 (2)
- 1980 (1)
all
top 3
Main Field
- 68-XX (226)
- 03-XX (87)
- 00-XX (11)
- 65-XX (5)
- 91-XX (5)
- 94-XX (4)
- 51-XX (3)
- 90-XX (3)
- 01-XX (2)
- 06-XX (2)
- 08-XX (2)
- 11-XX (2)
- 18-XX (2)
- 26-XX (2)
- 60-XX (2)
- 81-XX (2)
- 05-XX (1)
- 12-XX (1)
- 13-XX (1)
- 14-XX (1)
- 20-XX (1)
- 28-XX (1)
- 33-XX (1)
- 35-XX (1)
- 41-XX (1)
- 42-XX (1)
- 70-XX (1)
- 76-XX (1)
- 93-XX (1)
- 97-XX (1)
all
top 3
Software
- Coq (32)
- Isabelle/HOL (28)
- CLAM (25)
- Isabelle (24)
- Oyster (22)
- Nuprl (20)
- NQTHM (19)
- IsaCoSy (18)
- IsaPlanner (17)
- Theorema (14)
- HipSpec (13)
- InKa (13)
- TPTP (13)
- z3 (13)
- CVC4 (12)
- HOL (12)
- Isar (11)
- Mizar (11)
- HOL Light (10)
- OTTER (10)
- PVS (10)
- SPASS (10)
- SPIKE (10)
- Sledgehammer (10)
- GitHub (9)
- HR (9)
- LCF (9)
- VAMPIRE (9)
- Flyspeck (8)
- Hipster (8)
- Archive Formal Proofs (7)
- E Theorem Prover (7)
- ML (7)
- QuickCheck (7)
- RRL (7)
- SMT-LIB (7)
- ACL2 (6)
- Haskell (6)
- Lambda-Clam (6)
- Prodigy (6)
- TPS (6)
- kepler98 (6)
- Automath (5)
- Dr.Doodle (5)
- Waldmeister (5)
- Zeno (5)
- AProVE (4)
- ActiveMath (4)
- Bliksem (4)
- Cyclist (4)
- Dafny (4)
- HOLyHammer (4)
- LOUI (4)
- MAYA (4)
- ML4PG (4)
- MaSh (4)
- Mace4 (4)
- MathWeb (4)
- Mathematica (4)
- Proof General (4)
- Spacer (4)
- Z (4)
- ALISA (3)
- GRAFFITI (3)
- Geometer's Sketchpad (3)
- Hyperproof (3)
- Isabelle/Isar (3)
- LEGO (3)
- MML (3)
- Maple (3)
- Mathpert (3)
- Matita (3)
- Metis_ (3)
- OCaml (3)
- OMDoc (3)
- Omega-MKRP (3)
- PLAGIATOR (3)
- PRMLT (3)
- RAHFT (3)
- SETHEO (3)
- TacticToe (3)
- VeriFun (3)
- VeriMAP (3)
- WEKA (3)
- Whelp (3)
- Why3 (3)
- Yices (3)
- AVATAR (2)
- Analytica (2)
- Boogie (2)
- C4.5 (2)
- CASL (2)
- Caduceus (2)
- CafeOBJ (2)
- Cambridge LCF (2)
- Cinderella (2)
- Clingo (2)
- Coq/SSReflect (2)
- CoqHammer (2)
- ESC/Java (2)
- and 298 more Software Packages
