Search results for "Theorem-Proving"

Hits ?▲	Authors	Title	Venue	Year	Link
19	Guillaume Lample, Timothée Lacroix, Marie-Anne Lachaux, Aurélien Rodriguez, Amaury Hayat, Thibaut Lavril, Gabriel Ebner, Xavier Martinet	HyperTree Proof Search for Neural Theorem Proving.	NeurIPS	2022	DBLP BibTeX RDF
19	José Meseguer 0001	Checking Sufficient Completeness by Inductive Theorem Proving.	WRLA@ETAPS	2022	DBLP DOI BibTeX RDF
19	Mark Chevallier, Matthew Whyte, Jacques D. Fleuriot	Constrained Training of Neural Networks via Theorem Proving.	OVERLAY@AI*IA	2022	DBLP BibTeX RDF
19	Jesse Michael Han, Jason Rute, Yuhuai Wu, Edward W. Ayers, Stanislas Polu	Proof Artifact Co-Training for Theorem Proving with Language Models.	ICLR	2022	DBLP BibTeX RDF
19	Klaus Miesenberger, Walther Neuper, Bernhard Stöger, Makarius Wenzel	Towards an Accessible Mathematics Working Environment Based on Isabelle/VSCode.	ThEdu@FLoC	2022	DBLP DOI BibTeX RDF
19	Ankit Kumar, Andrew T. Walter, Panagiotis Manolios	Automated Grading of Automata with ACL2s.	ThEdu@FLoC	2022	DBLP DOI BibTeX RDF
19	Joomy Korkut	A Proof Tree Builder for Sequent Calculus and Hoare Logic.	ThEdu@FLoC	2022	DBLP DOI BibTeX RDF
19	Thierry N. Dana-Picard	Computer Assisted Proofs and Automated Methods in Mathematics Education.	ThEdu@FLoC	2022	DBLP DOI BibTeX RDF
19	Joana Teles, Vanda Santos, Pedro Quaresma	A Rule Based Theorem Prover: an Introduction to Proofs in Secondary Schools.	ThEdu@FLoC	2022	DBLP DOI BibTeX RDF
19	Frederik Krogsdal Jacobsen, Jørgen Villadsen	On Exams with the Isabelle Proof Assistant.	ThEdu@FLoC	2022	DBLP DOI BibTeX RDF
19	Davi Romero de Vasconcelos	ANITA: Analytic Tableau Proof Assistant.	ThEdu@FLoC	2022	DBLP DOI BibTeX RDF
19	Frédéric Dupuis, Robert Y. Lewis, Heather Macbeth	Formalized functional analysis with semilinear maps.	ITP	2022	DBLP DOI BibTeX RDF
19	Yury Kudryashov	Formalizing the Divergence Theorem and the Cauchy Integral Formula in Lean.	ITP	2022	DBLP DOI BibTeX RDF
19	Nicolas Magaud	Proof Pearl: Formalizing Spreads and Packings of the Smallest Projective Space PG(3, 2) Using the Coq Proof Assistant.	ITP	2022	DBLP DOI BibTeX RDF
19	Chelsea Edmonds, Lawrence C. Paulson	Formalising Fisher's Inequality: Formal Linear Algebraic Proof Techniques in Combinatorics.	ITP	2022	DBLP DOI BibTeX RDF
19	Dominik Kirst	Computational Back-And-Forth Arguments in Constructive Type Theory.	ITP	2022	DBLP DOI BibTeX RDF
19	Oskar Abrahamsson, Magnus O. Myreen, Ramana Kumar, Thomas Sewell	Candle: A Verified Implementation of HOL Light.	ITP	2022	DBLP DOI BibTeX RDF
19	Arve Gengelbach, Johannes Åman Pohjola	A Verified Cyclicity Checker: For Theories with Overloaded Constants.	ITP	2022	DBLP DOI BibTeX RDF
19	Amy P. Felty	Modelling and Verifying Properties of Biological Neural Networks (Invited Talk).	ITP	2022	DBLP DOI BibTeX RDF
19	Malgorzata Biernacka, Witold Charatonik, Tomasz Drab	The Zoo of Lambda-Calculus Reduction Strategies, And Coq.	ITP	2022	DBLP DOI BibTeX RDF
19	Hrutvik Kanabar, Anthony C. J. Fox, Magnus O. Myreen	Taming an Authoritative Armv8 ISA Specification: L3 Validation and CakeML Compiler Verification.	ITP	2022	DBLP DOI BibTeX RDF
19	Asta Halkjær From, Frederik Krogsdal Jacobsen	Verifying a Sequent Calculus Prover for First-Order Logic with Functions in Isabelle/HOL.	ITP	2022	DBLP DOI BibTeX RDF
19	Koundinya Vajjha, Barry M. Trager, Avraham Shinnar, Vasily Pestun	Formalization of a Stochastic Approximation Theorem.	ITP	2022	DBLP DOI BibTeX RDF
19	Martin Desharnais, Petar Vukmirovic, Jasmin Blanchette, Makarius Wenzel	Seventeen Provers Under the Hammer.	ITP	2022	DBLP DOI BibTeX RDF
19	Anne Baanen	Use and Abuse of Instance Parameters in the Lean Mathematical Library.	ITP	2022	DBLP DOI BibTeX RDF
19	Johannes Hostert, Andrej Dudenhefner, Dominik Kirst	Undecidability of Dyadic First-Order Logic in Coq.	ITP	2022	DBLP DOI BibTeX RDF
19	Bohua Zhan	User Interface Design in the HolPy Theorem Prover (Invited Talk).	ITP	2022	DBLP DOI BibTeX RDF
19	Kazuhiko Sakaguchi	Reflexive Tactics for Algebra, Revisited.	ITP	2022	DBLP DOI BibTeX RDF
19	Peter Lammich	Refinement of Parallel Algorithms down to LLVM.	ITP	2022	DBLP DOI BibTeX RDF
19	Karol Pak, Cezary Kaliszyk	Formalizing a Diophantine Representation of the Set of Prime Numbers.	ITP	2022	DBLP DOI BibTeX RDF
19	Emin Karayel	Formalization of Randomized Approximation Algorithms for Frequency Moments.	ITP	2022	DBLP DOI BibTeX RDF
19	Bohua Zhan, Yi Lv, Shuling Wang, Gehang Zhao, Jifeng Hao, Hong Ye, Bican Xia	Compositional Verification of Interacting Systems Using Event Monads.	ITP	2022	DBLP DOI BibTeX RDF
19	Alley Stoughton, Carol Chen, Marco Gaboardi, Weihao Qu	Formalizing Algorithmic Bounds in the Query Model in EasyCrypt.	ITP	2022	DBLP DOI BibTeX RDF
19	Jason Gross, Théo Zimmermann, Miraya Poddar-Agrawal, Adam Chlipala	Automatic Test-Case Reduction in Proof Assistants: A Case Study in Coq.	ITP	2022	DBLP DOI BibTeX RDF
19	Jagadish Bapanapally, Ruben Gamboa	A Complete, Mechanically-Verified Proof of the Banach-Tarski Theorem in ACL2(R).	ITP	2022	DBLP DOI BibTeX RDF
19	Heiko Becker, Mohit Tekriwal, Eva Darulova, Anastasia Volkova, Jean-Baptiste Jeannin	Dandelion: Certified Approximations of Elementary Functions.	ITP	2022	DBLP DOI BibTeX RDF
19	Jared Yeager, J. Eliot B. Moss, Michael Norrish, Philip S. Thomas	Mechanizing Soundness of Off-Policy Evaluation.	ITP	2022	DBLP DOI BibTeX RDF
19	Jacob Prinz, G. A. Kavvos, Leonidas Lampropoulos	Deeper Shallow Embeddings.	ITP	2022	DBLP DOI BibTeX RDF
19	Yaël Dillies, Bhavik Mehta	Formalising Szemerédi's Regularity Lemma in Lean.	ITP	2022	DBLP DOI BibTeX RDF
19		Front Matter, Table of Contents, Preface, Conference Organization.	ITP	2022	DBLP DOI BibTeX RDF
19	Johannes Åman Pohjola, Alejandro Gómez-Londoño, James Shaker, Michael Norrish	Kalas: A Verified, End-To-End Compiler for a Choreographic Language.	ITP	2022	DBLP DOI BibTeX RDF
19	Zarathustra Amadeus Goertzel, Jan Jakubuv, Cezary Kaliszyk, Miroslav Olsák, Jelle Piepenbrock, Josef Urban	The Isabelle ENIGMA.	ITP	2022	DBLP DOI BibTeX RDF
19	Yannick Forster 0002, Fabian Kunze, Nils Lauermann	Synthetic Kolmogorov Complexity in Coq.	ITP	2022	DBLP DOI BibTeX RDF
19	María Inés de Frutos-Fernández	Formalizing the Ring of Adèles of a Global Field.	ITP	2022	DBLP DOI BibTeX RDF
19	Jason Gross, Andres Erbsen, Jade Philipoom, Miraya Poddar-Agrawal, Adam Chlipala	Accelerating Verified-Compiler Development with a Verified Rewriting Engine.	ITP	2022	DBLP DOI BibTeX RDF
19	Geoff Sutcliffe	The 10th IJCAR automated theorem proving system competition - CASC-J10.	AI Commun.	2021	DBLP DOI BibTeX RDF
19	Geoff Sutcliffe, Martin Desharnais	The CADE-28 Automated Theorem Proving System Competition - CASC-28.	AI Commun.	2021	DBLP DOI BibTeX RDF
19	Thierry Coquand, Hajime Ishihara, Sara Negri, Peter M. Schuster	Geometric Logic, Constructivisation, and Automated Theorem Proving (Dagstuhl Seminar 21472).	Dagstuhl Reports	2021	DBLP DOI BibTeX RDF
19	Ayesha Gauhar, Adnan Rashid, Osman Hasan, João Bispo, João M. P. Cardoso	Formal verification of Matrix based MATLAB models using interactive theorem proving.	PeerJ Comput. Sci.	2021	DBLP DOI BibTeX RDF
19	Mishal Fatima Minhas, Osman Hasan, Sa'ed Abed	HVoC: a Hybrid Model Checking - Interactive Theorem Proving Approach for Functional Verification of Digital Circuits.	J. Electron. Test.	2021	DBLP DOI BibTeX RDF
19	Sean B. Holden	Machine Learning for Automated Theorem Proving: Learning to Solve SAT and QSAT.	Found. Trends Mach. Learn.	2021	DBLP DOI BibTeX RDF
19	Sean Welleck, Jiacheng Liu 0010, Ronan Le Bras 0001, Hannaneh Hajishirzi, Yejin Choi 0001, Kyunghyun Cho	NaturalProofs: Mathematical Theorem Proving in Natural Language.	CoRR	2021	DBLP BibTeX RDF
19	Yuanrui Zhang	A Dynamic Logic for Verification of Synchronous Models based on Theorem Proving.	CoRR	2021	DBLP BibTeX RDF
19	Jelle Piepenbrock, Tom Heskes, Mikolás Janota, Josef Urban	Learning Equational Theorem Proving.	CoRR	2021	DBLP BibTeX RDF
19	Wolfgang Windsteiger	Automated Theorem Proving in the Classroom.	ADG	2021	DBLP DOI BibTeX RDF
19	Ujala Qasim, Adnan Rashid, Osman Hasan	Formalization of Bond Graph using Higher-order-logic Theorem Proving.	CoRR	2021	DBLP BibTeX RDF
19	Shahid Ali Murtza, Waqar Ahmed, Adnan Rashid, Osman Hasan	Towards the Formal Performance Analysis of Multistate Coherent Systems using HOL Theorem Proving.	CoRR	2021	DBLP BibTeX RDF
19	Amrith Krishna, Sebastian Riedel 0001, Andreas Vlachos 0001	ProoFVer: Natural Logic Theorem Proving for Fact Verification.	CoRR	2021	DBLP BibTeX RDF
19	Stanislaw J. Purgal, Julian Parsert, Cezary Kaliszyk	A Study of Continuous Vector Representationsfor Theorem Proving.	CoRR	2021	DBLP BibTeX RDF
19	Cheuk Ting Li	An Automated Theorem Proving Framework for Information-Theoretic Results.	CoRR	2021	DBLP BibTeX RDF
19	Joseph A. Goguen	Theorem Proving and Algebra.	CoRR	2021	DBLP BibTeX RDF
19	Chantal Keller, Mathias Fleury (eds.)	Proceedings Seventh Workshop on Proof eXchange for Theorem Proving, PxTP 2021, Pittsburg, PA, USA, July 11, 2021.	PxTP	2021	DBLP DOI BibTeX RDF
19	Karel Chvalovský, Jan Jakubuv, Miroslav Olsák, Josef Urban	Learning Theorem Proving Components.	CoRR	2021	DBLP BibTeX RDF
19	Jesse Michael Han, Jason Rute, Yuhuai Wu, Edward W. Ayers, Stanislas Polu	Proof Artifact Co-training for Theorem Proving with Language Models.	CoRR	2021	DBLP BibTeX RDF
19	Mohamed Abdelghany, Sofiène Tahar	Formal FT-based Cause-Consequence Reliability Analysis using Theorem Proving.	CoRR	2021	DBLP BibTeX RDF
19	Stefan Hetzl, Jannik Vierling	Induction and Skolemization in saturation theorem proving.	CoRR	2021	DBLP BibTeX RDF
19	Stanislaw J. Purgal, Julian Parsert, Cezary Kaliszyk	A study of continuous vector representations for theorem proving.	J. Log. Comput.	2021	DBLP DOI BibTeX RDF
19	Adnan Rashid, Osman Hasan	Formal analysis of the continuous dynamics of cyber-physical systems using theorem proving.	J. Syst. Archit.	2021	DBLP DOI BibTeX RDF
19	Diego Marmsoler	Compositional Verification using Model Checking and Theorem Proving.	Model-Based Engineering of Collaborative Embedded Systems	2021	DBLP DOI BibTeX RDF
19	Kangfeng Ye, Simon Foster 0001, Jim Woodcock 0001	Automated Reasoning for Probabilistic Sequential Programs with Theorem Proving.	RAMiCS	2021	DBLP DOI BibTeX RDF
19	Stefan Mitsch, Xiangyu Jin, Bohua Zhan, Shuling Wang, Naijun Zhan	ARCH-COMP21 Category Report: Hybrid Systems Theorem Proving.	ARCH@ADHS	2021	DBLP DOI BibTeX RDF
19	Cheuk Ting Li	An Automated Theorem Proving Framework for Information-Theoretic Results.	ISIT	2021	DBLP DOI BibTeX RDF
19	Maxwell Crouse, Ibrahim Abdelaziz, Bassem Makni, Spencer Whitehead, Cristina Cornelio, Pavan Kapanipathi, Kavitha Srinivas, Veronika Thost, Michael Witbrock, Achille Fokoue	A Deep Reinforcement Learning Approach to First-Order Logic Theorem Proving.	AAAI	2021	DBLP DOI BibTeX RDF
19	Dohan Kim 0001, Christopher Lynch	Equational Theorem Proving Modulo.	CADE	2021	DBLP DOI BibTeX RDF
19	David A. Plaisted	Search Spaces for Theorem Proving Strategies.	ARCADE@CADE	2021	DBLP BibTeX RDF
19	Karel Chvalovský, Jan Jakubuv, Miroslav Olsák, Josef Urban	Learning Theorem Proving Components.	TABLEAUX	2021	DBLP DOI BibTeX RDF
19	Alexander Birch Jensen, Koen V. Hindriks, Jørgen Villadsen	On using Theorem Proving for Cognitive Agent-oriented Programming.	ICAART (1)	2021	DBLP DOI BibTeX RDF
19	Liron Cohen 0001, Cezary Kaliszyk (eds.)	12th International Conference on Interactive Theorem Proving, ITP 2021, June 29 to July 1, 2021, Rome, Italy (Virtual Conference).	ITP	2021	DBLP BibTeX RDF
19	Sean Welleck, Jiacheng Liu 0010, Ronan Le Bras 0001, Hanna Hajishirzi, Yejin Choi 0001, Kyunghyun Cho	NaturalProofs: Mathematical Theorem Proving in Natural Language.	NeurIPS Datasets and Benchmarks	2021	DBLP BibTeX RDF
19	Clare Dixon	Theorem Proving Using Clausal Resolution: From Past to Present.	RP	2021	DBLP DOI BibTeX RDF
19	Alexander Birch Jensen	A Theorem Proving Approach to Formal Verification of a Cognitive Agent.	DCAI (1)	2021	DBLP DOI BibTeX RDF
19	Yuhuai Wu, Albert Q. Jiang, Jimmy Ba, Roger Baker Grosse	INT: An Inequality Benchmark for Evaluating Generalization in Theorem Proving.	ICLR	2021	DBLP BibTeX RDF
19	Edvard K. Holden, Konstantin Korovin	Heterogeneous Heuristic Optimisation and Scheduling for First-Order Theorem Proving.	CICM	2021	DBLP DOI BibTeX RDF
19	Stanislaw J. Purgal	Deep Learning for Automated Theorem Proving - Extended Abstract.	CICM Workshops	2021	DBLP BibTeX RDF
19	Fabian Huch	Structure in Theorem Proving: Analyzing and Improving the Isabelle Archive of Formal Proofs - Extended Abstract (short paper).	CICM Workshops	2021	DBLP BibTeX RDF
19	Ahmed Bhayat	Automated theorem proving in higher-order logic		2021	RDF
19	Hans-Jörg Schurr, Mathias Fleury, Haniel Barbosa, Pascal Fontaine	Alethe: Towards a Generic SMT Proof Format (extended abstract).	PxTP	2021	DBLP DOI BibTeX RDF
19	Quentin Garchery	A Framework for Proof-carrying Logical Transformations.	PxTP	2021	DBLP DOI BibTeX RDF
19	Nicolas Magaud	Integrating an Automated Prover for Projective Geometry as a New Tactic in the Coq Proof Assistant.	PxTP	2021	DBLP DOI BibTeX RDF
19	Valentin Blot, Louise Dubois de Prisque, Chantal Keller, Pierre Vial	General Automation in Coq through Modular Transformations.	PxTP	2021	DBLP DOI BibTeX RDF
19	Maria Paola Bonacina	Proof Generation in CDSAT.	PxTP	2021	DBLP DOI BibTeX RDF
19	Stephan Gocht, Jakob Nordström, Ruben Martins	Certifying CNF Encodings of Pseudo-Boolean Constraints (abstract).	PxTP	2021	DBLP DOI BibTeX RDF
19	Merlin Carl, Hinrich Lorenzen, Michael Schmitz	Natural Language Proof Checking in Introduction to Proof Classes - First Experiences with Diproche.	ThEdu@CADE	2021	DBLP DOI BibTeX RDF
19	Clemens Eisenhofer, Martin Riener	Automated Instantiation of Control Flow Tracing Exercises.	ThEdu@CADE	2021	DBLP DOI BibTeX RDF
19	John Tang Boyland	Evolution of SASyLF 2008-2021.	ThEdu@CADE	2021	DBLP DOI BibTeX RDF
19	Zoltán Kovács, Róbert Vajda	Symbolic Comparison of Geometric Quantities in GeoGebra.	ThEdu@CADE	2021	DBLP DOI BibTeX RDF
19	Pedro Quaresma, Vanda Santos	Four Geometry Problems to Introduce Automated Deduction in Secondary Schools.	ThEdu@CADE	2021	DBLP DOI BibTeX RDF
19	Jørgen Villadsen, Asta Halkjær From, Patrick Blackburn	Teaching Intuitionistic and Classical Propositional Logic Using Isabelle.	ThEdu@CADE	2021	DBLP DOI BibTeX RDF
19	Zoltán Kovács, Jonathan H. Yu	Automated Discovery of Geometrical Theorems in GeoGebra.	ThEdu@CADE	2021	DBLP DOI BibTeX RDF
19	Konrad Slind	Specifying Message Formats with Contiguity Types.	ITP	2021	DBLP DOI BibTeX RDF