|
|
|
|
Venues (Conferences, Journals, ...)
|
|
|
GrowBag graphs for keyword ? (Num. hits/coverage)
Group by:
The graphs summarize 1960 occurrences of 846 keywords
|
|
|
|
|
Results
Found 3383 publication records. Showing 3383 according to the selection in the facets
| Hits ?▲ |
Authors |
Title |
Venue |
Year |
Link |
Author keywords |
| 19 | Tadayuki Yoshida, Ekawit Nantajeewarawat, Masaharu Munetomo, Kiyoshi Akama |
Logical Approach to Theorem Proving with Term Rewriting on KR-logic.  |
KEOD  |
2019 |
DBLP DOI BibTeX RDF |
|
| 19 | Stefan Mitsch, Andrew Sogokon, Yong Kiam Tan, Xiangyu Jin, Bohua Zhan, Shuling Wang, Naijun Zhan |
ARCH-COMP19 Category Report: Hybrid Systems Theorem Proving. |
ARCH@CPSIoTWeek |
2019 |
DBLP DOI BibTeX RDF |
|
| 19 | Mark R. Greenstreet |
Integrating SMT with Theorem Proving for Verification of Analog and Mixed-Signal Circuits (Invited Tutorial). |
FMCAD |
2019 |
DBLP DOI BibTeX RDF |
|
| 19 | Waqar Ahmad, Shahid Ali Murtza, Osman Hasan, Sofiène Tahar |
On the formalization of importance measures using HOL theorem proving. |
FormaliSE@ICSE |
2019 |
DBLP DOI BibTeX RDF |
|
| 19 | Daniel Huang 0001, Prafulla Dhariwal, Dawn Song, Ilya Sutskever |
GamePad: A Learning Environment for Theorem Proving. |
ICLR (Poster) |
2019 |
DBLP BibTeX RDF |
|
| 19 | Kshitij Bansal, Sarah M. Loos, Markus N. Rabe, Christian Szegedy, Stewart Wilcox |
HOList: An Environment for Machine Learning of Higher Order Logic Theorem Proving. |
ICML |
2019 |
DBLP BibTeX RDF |
|
| 19 | Agnieszka Slowik, Chaitanya Mangla, Mateja Jamnik, Sean B. Holden, Lawrence C. Paulson |
Bayesian Optimisation for Heuristic Configuration in Automated Theorem Proving. |
Vampire |
2019 |
DBLP BibTeX RDF |
|
| 19 | Jonas Betzendahl |
Definedness Reasoning in Formal Mathematics and Theorem Proving. |
CICM Workshops |
2019 |
DBLP BibTeX RDF |
|
| 19 | Fadil Kallat, Tristan Schäfer, Anna Vasileva |
CLS-SMT: Bringing Together Combinatory Logic Synthesis and Satisfiability Modulo Theories. |
PxTP |
2019 |
DBLP DOI BibTeX RDF |
|
| 19 | Eunice Palmeira da Silva, Fred Freitas, Jens Otten |
Converting ALC Connection Proofs into ALC Sequents. |
PxTP |
2019 |
DBLP DOI BibTeX RDF |
|
| 19 | Mathias Fleury, Hans-Jörg Schurr |
Reconstructing veriT Proofs in Isabelle/HOL. |
PxTP |
2019 |
DBLP DOI BibTeX RDF |
|
| 19 | Mohamed Yacine El Haddad, Guillaume Burel, Frédéric Blanqui |
EKSTRAKTO A tool to reconstruct Dedukti proofs from TSTP files (extended abstract). |
PxTP |
2019 |
DBLP DOI BibTeX RDF |
|
| 19 | Burak Ekici, Arjun Viswanathan, Yoni Zohar, Clark W. Barrett, Cesare Tinelli |
Verifying Bit-vector Invertibility Conditions in Coq (Extended Abstract). |
PxTP |
2019 |
DBLP DOI BibTeX RDF |
|
| 19 | Ludovic Font, Sébastien Cyr, Philippe R. Richard, Michel Gagnon |
Automating the Generation of High School Geometry Proofs using Prolog in an Educational Context. |
ThEdu@CADE |
2019 |
DBLP DOI BibTeX RDF |
|
| 19 | Asta Halkjær From, Alexander Birch Jensen, Anders Schlichtkrull, Jørgen Villadsen |
Teaching a Formalized Logical Calculus. |
ThEdu@CADE |
2019 |
DBLP DOI BibTeX RDF |
|
| 19 | Nuno Baeta, Pedro Quaresma, Zoltán Kovács |
Towards a Geometry Automated Provers Competition. |
ThEdu@CADE |
2019 |
DBLP DOI BibTeX RDF |
|
| 19 | David M. Cerna, Rafael P. D. Kiesel, Alexandra Dzhiganskaya |
A Mobile Application for Self-Guided Study of Formal Reasoning. |
ThEdu@CADE |
2019 |
DBLP DOI BibTeX RDF |
|
| 19 | Josje Lodder, Bastiaan Heeren, Johan Jeuring |
Providing Hints, Next Steps and Feedback in a Tutoring System for Structural Induction. |
ThEdu@CADE |
2019 |
DBLP DOI BibTeX RDF |
|
| 19 | Sarah Winkler, Aart Middeldorp |
Tools in Term Rewriting for Education. |
ThEdu@CADE |
2019 |
DBLP DOI BibTeX RDF |
|
| 19 | Matthias Brun 0002, Dmitriy Traytel |
Generic Authenticated Data Structures, Formally. |
ITP |
2019 |
DBLP DOI BibTeX RDF |
|
| 19 | Chad E. Brown, Cezary Kaliszyk, Karol Pak |
Higher-Order Tarski Grothendieck as a Foundation for Formal Proof. |
ITP |
2019 |
DBLP DOI BibTeX RDF |
|
| 19 | Jonas Bayer, Marco David, Abhik Pal, Benedikt Stock, Dierk Schleicher |
The DPRM Theorem in Isabelle (Short Paper). |
ITP |
2019 |
DBLP DOI BibTeX RDF |
|
| 19 | Peter Lammich, Tobias Nipkow |
Proof Pearl: Purely Functional, Simple and Efficient Priority Search Trees and Applications to Prim and Dijkstra. |
ITP |
2019 |
DBLP DOI BibTeX RDF |
|
| 19 | Johannes Åman Pohjola, Henrik Rostedt, Magnus O. Myreen |
Characteristic Formulae for Liveness Properties of Non-Terminating CakeML Programs. |
ITP |
2019 |
DBLP DOI BibTeX RDF |
|
| 19 | Reynald Affeldt, Jacques Garrigue, Xuanrui Qi, Kazunari Tanaka |
Proving Tree Algorithms for Succinct Data Structures. |
ITP |
2019 |
DBLP DOI BibTeX RDF |
|
| 19 | Sander R. Dahmen, Johannes Hölzl, Robert Y. Lewis |
Formalizing the Solution to the Cap Set Problem. |
ITP |
2019 |
DBLP DOI BibTeX RDF |
|
| 19 | Martin Dixon |
An Increasing Need for Formality (Invited Talk). |
ITP |
2019 |
DBLP DOI BibTeX RDF |
|
| 19 | Robert Sison, Toby Murray |
Verifying That a Compiler Preserves Concurrent Value-Dependent Information-Flow Security. |
ITP |
2019 |
DBLP DOI BibTeX RDF |
|
| 19 | Sam Lasser, Chris Casinghino, Kathleen Fisher, Cody Roux |
A Verified LL(1) Parser Generator. |
ITP |
2019 |
DBLP DOI BibTeX RDF |
|
| 19 | Akihisa Yamada 0002, Jérémy Dubut |
Complete Non-Orders and Fixed Points. |
ITP |
2019 |
DBLP DOI BibTeX RDF |
|
| 19 | Guillaume Bertholon, Érik Martin-Dorel, Pierre Roux |
Primitive Floats in Coq. |
ITP |
2019 |
DBLP DOI BibTeX RDF |
|
| 19 | Jan Jakubuv, Josef Urban |
Hammering Mizar by Learning Clause Guidance (Short Paper). |
ITP |
2019 |
DBLP DOI BibTeX RDF |
|
| 19 | Kevin Buzzard |
What Makes a Mathematician Tick? (Invited Talk). |
ITP |
2019 |
DBLP DOI BibTeX RDF |
|
| 19 | Enrico Tassi |
Deriving Proved Equality Tests in Coq-Elpi: Stronger Induction Principles for Containers in Coq. |
ITP |
2019 |
DBLP DOI BibTeX RDF |
|
| 19 | Mohammad Abdulaziz, Charles Gretton, Michael Norrish |
A Verified Compositional Algorithm for AI Planning. |
ITP |
2019 |
DBLP DOI BibTeX RDF |
|
| 19 | |
Front Matter, Table of Contents, Preface, Conference Organization. |
ITP |
2019 |
DBLP DOI BibTeX RDF |
|
| 19 | Jesse Michael Han, Floris van Doorn |
A Formalization of Forcing and the Unprovability of the Continuum Hypothesis. |
ITP |
2019 |
DBLP DOI BibTeX RDF |
|
| 19 | Talia Ringer, Nathaniel Yazdani, John Leo, Dan Grossman |
Ornaments for Proof Reuse in Coq. |
ITP |
2019 |
DBLP DOI BibTeX RDF |
|
| 19 | Peter Lammich |
Generating Verified LLVM from Isabelle/HOL. |
ITP |
2019 |
DBLP DOI BibTeX RDF |
|
| 19 | Julian Brunner 0001, Benedikt Seidl, Salomon Sickert |
A Verified and Compositional Translation of LTL to Deterministic Rabin Automata. |
ITP |
2019 |
DBLP DOI BibTeX RDF |
|
| 19 | Cezary Kaliszyk, Karol Pak |
Declarative Proof Translation (Short Paper). |
ITP |
2019 |
DBLP DOI BibTeX RDF |
|
| 19 | Mihir Parang Mehta, William R. Cook |
Binary-Compatible Verification of Filesystems with ACL2. |
ITP |
2019 |
DBLP DOI BibTeX RDF |
|
| 19 | Florian Steinberg 0001, Laurent Théry, Holger Thies |
Quantitative Continuity and Computable Analysis in Coq. |
ITP |
2019 |
DBLP DOI BibTeX RDF |
|
| 19 | Jeremy Avigad, Mario Carneiro, Simon Hudon |
Data Types as Quotients of Polynomial Functors. |
ITP |
2019 |
DBLP DOI BibTeX RDF |
|
| 19 | Florent Bréhard, Assia Mahboubi, Damien Pous |
A Certificate-Based Approach to Formally Verified Approximations. |
ITP |
2019 |
DBLP DOI BibTeX RDF |
|
| 19 | Ran Chen, Cyril Cohen, Jean-Jacques Lévy, Stephan Merz, Laurent Théry |
Formal Proofs of Tarjan's Strongly Connected Components Algorithm in Why3, Coq and Isabelle. |
ITP |
2019 |
DBLP DOI BibTeX RDF |
|
| 19 | Lukasz Czajka 0001 |
First-Order Guarded Coinduction in Coq. |
ITP |
2019 |
DBLP DOI BibTeX RDF |
|
| 19 | Mario Carneiro |
Formalizing Computability Theory via Partial Recursive Functions. |
ITP |
2019 |
DBLP DOI BibTeX RDF |
|
| 19 | Manuel Eberl |
Nine Chapters of Analytic Number Theory in Isabelle/HOL. |
ITP |
2019 |
DBLP DOI BibTeX RDF |
|
| 19 | Minchao Wu, Rajeev Goré |
Verified Decision Procedures for Modal Logics. |
ITP |
2019 |
DBLP DOI BibTeX RDF |
|
| 19 | Yannick Forster 0002, Fabian Kunze |
A Certifying Extraction with Time Bounds from Coq to Call-By-Value Lambda Calculus. |
ITP |
2019 |
DBLP DOI BibTeX RDF |
|
| 19 | Daniel E. Severín |
Formalization of the Domination Chain with Weighted Parameters (Short Paper). |
ITP |
2019 |
DBLP DOI BibTeX RDF |
|
| 19 | Maximilian P. L. Haslbeck, Peter Lammich |
Refinement with Time - Refining the Run-Time of Algorithms in Isabelle/HOL. |
ITP |
2019 |
DBLP DOI BibTeX RDF |
|
| 19 | June Andronick |
A Million Lines of Proof About a Moving Target (Invited Talk). |
ITP |
2019 |
DBLP DOI BibTeX RDF |
|
| 19 | Fabian Immler, Jonas Rädle, Makarius Wenzel |
Virtualization of HOL4 in Isabelle. |
ITP |
2019 |
DBLP DOI BibTeX RDF |
|
| 19 | Armaël Guéneau, Jacques-Henri Jourdan, Arthur Charguéraud, François Pottier |
Formal Proof and Analysis of an Incremental Cycle Detection Algorithm. |
ITP |
2019 |
DBLP DOI BibTeX RDF |
|
| 19 | Geoff Sutcliffe |
The 9th IJCAR Automated Theorem Proving System Competition - CASC-J9. |
AI Commun. |
2018 |
DBLP DOI BibTeX RDF |
|
| 19 | Jan Jakubuv, Josef Urban |
Hierarchical invention of theorem proving strategies. |
AI Commun. |
2018 |
DBLP DOI BibTeX RDF |
|
| 19 | Zheng Yang 0007, Hang Lei |
Optimization of Executable Formal Interpreters Developed in Higher-Order Logic Theorem Proving Systems. |
IEEE Access |
2018 |
DBLP DOI BibTeX RDF |
|
| 19 | José de Jesús Lavalle-Martínez, Manuel Montes-y-Gómez, Héctor Jiménez-Salazar, Luis Villaseñor Pineda, Beatríz Beltrán Martínez |
Automatic Theorem Proving for Natural Logic: a Case Study on Textual Entailment. |
Computación y Sistemas |
2018 |
DBLP DOI BibTeX RDF |
|
| 19 | Adnan Rashid, Osman Hasan |
Formal Analysis of Robotic Cell Injection Systems using Theorem Proving. |
CoRR |
2018 |
DBLP BibTeX RDF |
|
| 19 | Niki Vazou, Joachim Breitner, Will Kunkel, David Van Horn, Graham Hutton |
Functional Pearl: Theorem Proving for All (Equational Reasoning in Liquid Haskell). |
CoRR |
2018 |
DBLP BibTeX RDF |
|
| 19 | Pasquale Minervini, Matko Bosnjak, Tim Rocktäschel, Sebastian Riedel 0001 |
Towards Neural Theorem Proving at Scale. |
CoRR |
2018 |
DBLP BibTeX RDF |
|
| 19 | Andres Campero, Aldo Pareja, Tim Klinger, Josh Tenenbaum 0001, Sebastian Riedel 0001 |
Logical Rule Induction and Theory Learning Using Neural Theorem Proving. |
CoRR |
2018 |
DBLP BibTeX RDF |
|
| 19 | Mitsuru Kusumoto, Keisuke Yahata, Masahiro Sakai |
Automated Theorem Proving in Intuitionistic Propositional Logic by Deep Reinforcement Learning. |
CoRR |
2018 |
DBLP BibTeX RDF |
|
| 19 | Zheng Yang 0007, Hang Lei |
Optimization of Executable Formal Interpreters developed in Higher-order Theorem Proving Systems. |
CoRR |
2018 |
DBLP BibTeX RDF |
|
| 19 | Pedro Quaresma, Walther Neuper (eds.) |
Proceedings 6th International Workshop on Theorem proving components for Educational software, ThEdu@CADE 2017, Gothenburg, Sweden, 6 Aug 2017. |
ThEdu@CADE |
2018 |
DBLP BibTeX RDF |
|
| 19 | Michael Kinyon |
Proof Simplification and Automated Theorem Proving. |
CoRR |
2018 |
DBLP BibTeX RDF |
|
| 19 | Daniel Huang 0001, Prafulla Dhariwal, Dawn Song, Ilya Sutskever |
GamePad: A Learning Environment for Theorem Proving. |
CoRR |
2018 |
DBLP BibTeX RDF |
|
| 19 | Cezary Kaliszyk, Josef Urban, Henryk Michalewski, Mirek Olsák |
Reinforcement Learning of Theorem Proving. |
CoRR |
2018 |
DBLP BibTeX RDF |
|
| 19 | Zheng Yang 0007, Hang Lei |
A general formal memory framework in Coq for verifying the properties of programs based on higher-order logic theorem proving with increased automation, consistency, and reusability. |
CoRR |
2018 |
DBLP BibTeX RDF |
|
| 19 | Jeremy Avigad, Jasmin Christian Blanchette, Gerwin Klein, Lawrence C. Paulson, Andrei Popescu 0001, Gregor Snelting |
Introduction to Milestones in Interactive Theorem Proving. |
J. Autom. Reason. |
2018 |
DBLP DOI BibTeX RDF |
|
| 19 | Maria Paola Bonacina |
Parallel Theorem Proving. |
Handbook of Parallel Constraint Reasoning |
2018 |
DBLP DOI BibTeX RDF |
|
| 19 | Stefan Mitsch, Andrew Sogokon, Yong Kiam Tan, André Platzer, Hengjun Zhao, Xiangyu Jin, Shuling Wang, Naijun Zhan |
ARCH-COMP18 Category Report: Hybrid Systems Theorem Proving. |
ARCH@ADHS |
2018 |
DBLP DOI BibTeX RDF |
|
| 19 | Sumayya Shiraz, Osman Hasan |
Formal Verification of n-bit ALU Using Theorem Proving. |
SBMF |
2018 |
DBLP DOI BibTeX RDF |
|
| 19 | Jeremy Avigad, Assia Mahboubi (eds.) |
Interactive Theorem Proving - 9th International Conference, ITP 2018, Held as Part of the Federated Logic Conference, FloC 2018, Oxford, UK, July 9-12, 2018, Proceedings |
ITP |
2018 |
DBLP DOI BibTeX RDF |
|
| 19 | Cezary Kaliszyk, Josef Urban, Henryk Michalewski, Miroslav Olsák |
Reinforcement Learning of Theorem Proving. |
NeurIPS |
2018 |
DBLP BibTeX RDF |
|
| 19 | Yassmeen Elderhalli, Osman Hasan, Waqar Ahmad, Sofiène Tahar |
Formal Dynamic Fault Trees Analysis Using an Integration of Theorem Proving and Model Checking. |
NFM |
2018 |
DBLP DOI BibTeX RDF |
|
| 19 | Alper Altuntas, John W. Baugh Jr. |
Hybrid Theorem Proving as a Lightweight Method for Verifying Numerical Software. |
CORRECTNESS@SC |
2018 |
DBLP DOI BibTeX RDF |
|
| 19 | Niki Vazou, Joachim Breitner, Rose Kunkel, David Van Horn, Graham Hutton |
Theorem proving for all: equational reasoning in liquid Haskell (functional pearl). |
Haskell@ICFP |
2018 |
DBLP DOI BibTeX RDF |
|
| 19 | Yaqing Jiang, Petros Papapanagiotou, Jacques D. Fleuriot |
Machine Learning for Inductive Theorem Proving. |
AISC |
2018 |
DBLP DOI BibTeX RDF |
|
| 19 | Walther Neuper |
Technologies for "Complete, Transparent & Interactive Models of Math" in Education. |
ThEdu@FLoC |
2018 |
DBLP DOI BibTeX RDF |
|
| 19 | Maximilian Doré, Krysia Broda |
Towards Intuitive Reasoning in Axiomatic Geometry. |
ThEdu@FLoC |
2018 |
DBLP DOI BibTeX RDF |
|
| 19 | Nuno Baeta, Pedro Quaresma |
Towards Ranking Geometric Automated Theorem Provers. |
ThEdu@FLoC |
2018 |
DBLP DOI BibTeX RDF |
|
| 19 | Wolfgang Schreiner |
Theorem and Algorithm Checking for Courses on Logic and Formal Methods. |
ThEdu@FLoC |
2018 |
DBLP DOI BibTeX RDF |
|
| 19 | Jørgen Villadsen, Asta Halkjær From, Anders Schlichtkrull |
Natural Deduction Assistant (NaDeA). |
ThEdu@FLoC |
2018 |
DBLP DOI BibTeX RDF |
|
| 19 | Anders Schlichtkrull, Jørgen Villadsen, Asta Halkjær From |
Students' Proof Assistant (SPA). |
ThEdu@FLoC |
2018 |
DBLP DOI BibTeX RDF |
|
| 19 | Hira Taqdees Syeda, Gerwin Klein |
Program Verification in the Presence of Cached Address Translation. |
ITP |
2018 |
DBLP DOI BibTeX RDF |
|
| 19 | Callum Bannister, Peter Höfner, Gerwin Klein |
Backwards and Forwards with Separation Logic. |
ITP |
2018 |
DBLP DOI BibTeX RDF |
|
| 19 | Florian Meßner, Julian Parsert, Jonas Schöpf, Christian Sternagel |
A Formally Verified Solver for Homogeneous Linear Diophantine Equations. |
ITP |
2018 |
DBLP DOI BibTeX RDF |
|
| 19 | Alexander Knüppel, Thomas Thüm, Carsten Immanuel Pardylla, Ina Schaefer |
Understanding Parameters of Deductive Verification: An Empirical Investigation of KeY. |
ITP |
2018 |
DBLP DOI BibTeX RDF |
|
| 19 | Mariano M. Moscato, Carlos Gustavo López Pombo, César A. Muñoz, Marco A. Feliú |
Boosting the Reuse of Formal Specifications. |
ITP |
2018 |
DBLP DOI BibTeX RDF |
|
| 19 | Jinxu Zhao, Bruno C. d. S. Oliveira, Tom Schrijvers |
Formalization of a Polymorphic Subtyping Algorithm. |
ITP |
2018 |
DBLP DOI BibTeX RDF |
|
| 19 | Manuel Eberl, Max W. Haslbeck, Tobias Nipkow |
Verified Analysis of Random Binary Tree Structures. |
ITP |
2018 |
DBLP DOI BibTeX RDF |
|
| 19 | Raphaël Cauderlier |
Tactics and Certificates in Meta Dedukti. |
ITP |
2018 |
DBLP DOI BibTeX RDF |
|
| 19 | Reto Achermann, Lukas Humbel, David A. Cock, Timothy Roscoe |
Physical Addressing on Real Hardware in Isabelle/HOL. |
ITP |
2018 |
DBLP DOI BibTeX RDF |
|
| 19 | Ramana Kumar, Eric Mullen, Zachary Tatlock, Magnus O. Myreen |
Software Verification with ITPs Should Use Binary Code Extraction to Reduce the TCB - (Short Paper). |
ITP |
2018 |
DBLP DOI BibTeX RDF |
|
| 19 | Colm Baston, Venanzio Capretta |
The Coinductive Formulation of Common Knowledge. |
ITP |
2018 |
DBLP DOI BibTeX RDF |
|
| 19 | Abhishek Anand, Simon Boulier, Cyril Cohen, Matthieu Sozeau, Nicolas Tabareau |
Towards Certified Meta-Programming with Typed Template-Coq. |
ITP |
2018 |
DBLP DOI BibTeX RDF |
|
| 19 | Simon Wimmer 0001, Johannes Hölzl |
MDP + TA = PTA: Probabilistic Timed Automata, Formalized (Short Paper). |
ITP |
2018 |
DBLP DOI BibTeX RDF |
|
|
|
![[Valid RSS]](Pics/valid-rss.png "Validate my RSS feed")
data released under the ODC-BY 1.0 license