Search results for "theorem-proving"

Hits ?▲	Authors	Title	Venue	Year	Link
19	Floris van Doorn	Formalized Haar Measure.	ITP	2021	DBLP DOI BibTeX RDF
19	Lennard Gäher, Fabian Kunze	Mechanising Complexity Theory: The Cook-Levin Theorem in Coq.	ITP	2021	DBLP DOI BibTeX RDF
19	Matthias Brun 0002, Sára Decova, Andrea Lattuada, Dmitriy Traytel	Verified Progress Tracking for Timely Dataflow.	ITP	2021	DBLP DOI BibTeX RDF
19	Christian Doczkal	A Variant of Wagner's Theorem Based on Combinatorial Hypermaps.	ITP	2021	DBLP DOI BibTeX RDF
19	Andrei Popescu 0001, Thomas Bauereiss, Peter Lammich	Bounded-Deducibility Security (Invited Paper).	ITP	2021	DBLP DOI BibTeX RDF
19	Anne Baanen, Sander R. Dahmen, Ashvni Narayanan, Filippo A. E. Nuccio Mortarino Majno di Capriglio	A Formalization of Dedekind Domains and Class Groups of Global Fields.	ITP	2021	DBLP DOI BibTeX RDF
19	Raja Natarajan, Suneel Sarswat, Abhishek Kr Singh	Verified Double Sided Auctions for Financial Markets.	ITP	2021	DBLP DOI BibTeX RDF
19	Seulkee Baek	A Formally Verified Checker for First-Order Proofs.	ITP	2021	DBLP DOI BibTeX RDF
19		Front Matter, Table of Contents, Preface, Conference Organization.	ITP	2021	DBLP DOI BibTeX RDF
19	Sophie Bernard, Cyril Cohen, Assia Mahboubi, Pierre-Yves Strub	Unsolvability of the Quintic Formalized in Dependent Type Theory.	ITP	2021	DBLP DOI BibTeX RDF
19	Marco Maggesi, Cosimo Perini Brogi	A Formal Proof of Modal Completeness for Provability Logic.	ITP	2021	DBLP DOI BibTeX RDF
19	Edward W. Ayers, Mateja Jamnik, William T. Gowers	A Graphical User Interface Framework for Formal Verification.	ITP	2021	DBLP DOI BibTeX RDF
19	Christoph Benzmüller, David Fuenmayor	Value-Oriented Legal Argumentation in Isabelle/HOL.	ITP	2021	DBLP DOI BibTeX RDF
19	Laurent Théry	Proof Pearl : Playing with the Tower of Hanoi Formally.	ITP	2021	DBLP DOI BibTeX RDF
19	Dominik Kirst, Marc Hermes	Synthetic Undecidability and Incompleteness of First-Order Axiom Systems in Coq.	ITP	2021	DBLP DOI BibTeX RDF
19	Frédéric Besson	Itauto: An Extensible Intuitionistic SAT Solver.	ITP	2021	DBLP DOI BibTeX RDF
19	Hengchu Zhang, Wolf Honoré, Nicolas Koh, Yao Li 0004, Yishuai Li, Li-yao Xia, Lennart Beringer, William Mansky, Benjamin C. Pierce, Steve Zdancewic	Verifying an HTTP Key-Value Server with Interaction Trees and VST.	ITP	2021	DBLP DOI BibTeX RDF
19	Nadia Polikarpova	Synthesis of Safe Pointer-Manipulating Programs (Invited Talk).	ITP	2021	DBLP DOI BibTeX RDF
19	Yannick Forster 0002, Fabian Kunze, Gert Smolka, Maxi Wuttke	A Mechanised Proof of the Time Invariance Thesis for the Weak Call-By-Value λ-Calculus.	ITP	2021	DBLP DOI BibTeX RDF
19	Meven Lennon-Bertrand	Complete Bidirectional Typing for the Calculus of Inductive Constructions.	ITP	2021	DBLP DOI BibTeX RDF
19	Joshua Chen	Homotopy Type Theory in Isabelle.	ITP	2021	DBLP DOI BibTeX RDF
19	Andreas Lochbihler	A Mechanized Proof of the Max-Flow Min-Cut Theorem for Countable Networks.	ITP	2021	DBLP DOI BibTeX RDF
19	Katherine Cordwell, Yong Kiam Tan, André Platzer	A Verified Decision Procedure for Univariate Real Arithmetic with the BKR Algorithm.	ITP	2021	DBLP DOI BibTeX RDF
19	Luís Cruz-Filipe, Fabrizio Montesi, Marco Peressotti	Formalising a Turing-Complete Choreographic Language in Coq.	ITP	2021	DBLP DOI BibTeX RDF
19	Adrian De Lon, Peter Koepke, Anton Lorenzen	A Natural Formalization of the Mutilated Checkerboard Problem in Naproche.	ITP	2021	DBLP DOI BibTeX RDF
19	Pierre Nigron, Pierre-Évariste Dagand	Reaching for the Star: Tale of a Monad in Coq.	ITP	2021	DBLP DOI BibTeX RDF
19	Stepan Holub, Stepán Starosta	Formalization of Basic Combinatorics on Words.	ITP	2021	DBLP DOI BibTeX RDF
19	Kesha Hietala, Robert Rand 0001, Shih-Han Hung, Liyi Li 0002, Michael Hicks 0001	Proving Quantum Programs Correct.	ITP	2021	DBLP DOI BibTeX RDF
19	Czeslaw Bylinski, Artur Kornilowicz, Adam Naumowicz	Syntactic-Semantic Form of Mizar Articles.	ITP	2021	DBLP DOI BibTeX RDF
19	Luca Ciccone, Francesco Dagnino, Elena Zucca	Flexible Coinduction in Agda.	ITP	2021	DBLP DOI BibTeX RDF
19	César A. Muñoz, Mauricio Ayala-Rincón, Mariano M. Moscato, Aaron Dutle, Anthony J. Narkawicz, Ariane Alves Almeida, Andréia B. Avelar, Thiago Mendonça Ferreira Ramos	Formal Verification of Termination Criteria for First-Order Recursive Functions.	ITP	2021	DBLP DOI BibTeX RDF
19	Magnus O. Myreen	The CakeML Project's Quest for Ever Stronger Correctness Theorems (Invited Paper).	ITP	2021	DBLP DOI BibTeX RDF
19	Adnan Rashid, Muhammad Umair, Osman Hasan, Mohamed H. Zaki	Toward the Formalization of Macroscopic Models of Traffic Flow Using Higher-Order-Logic Theorem Proving.	IEEE Access	2020	DBLP DOI BibTeX RDF
19	Waqar Ahmad, Osman Hasan, Falah Awwad, Nabil Bastaki, Syed Rafay Hasan	Formal Reliability Analysis of an Integrated Power Generation System Using Theorem Proving.	IEEE Syst. J.	2020	DBLP DOI BibTeX RDF
19	Cinzia Bernardeschi, Andrea Domenici, Adriano Fagiolini, Maurizio Palmieri	Block-Based Models and Theorem Proving in Model-Based Development.	Electron. Commun. Eur. Assoc. Softw. Sci. Technol.	2020	DBLP DOI BibTeX RDF
19	Sebastian Ullrich 0002, Leonardo de Moura 0001	Beyond Notations: Hygienic Macro Expansion for Theorem Proving Languages.	CoRR	2020	DBLP BibTeX RDF
19	Yuhuai Wu, Albert Q. Jiang, Jimmy Ba, Roger B. Grosse	INT: An Inequality Benchmark for Evaluating Generalization in Theorem Proving.	CoRR	2020	DBLP BibTeX RDF
19	Bernhard Gleiss, Laura Kovács, Jakob Rath	Subsumption Demodulation in First-Order Theorem Proving.	CoRR	2020	DBLP BibTeX RDF
19	Pedro Quaresma, Walther Neuper, João Marcos 0001 (eds.)	Proceedings 9th International Workshop on Theorem Proving Components for Educational Software, ThEdu@IJCAR 2020, Paris, France, 29th June 2020.	ThEdu@IJCAR	2020	DBLP DOI BibTeX RDF
19	Ibrahim Abdelaziz, Veronika Thost, Maxwell Crouse, Achille Fokoue	An Experimental Study of Formula Embeddings for Automated Theorem Proving in First-Order Logic.	CoRR	2020	DBLP BibTeX RDF
19	Stanislas Polu, Ilya Sutskever	Generative Language Modeling for Automated Theorem Proving.	CoRR	2020	DBLP BibTeX RDF
19	Pedro Quaresma, Walther Neuper, João Marcos 0001 (eds.)	Proceedings 8th International Workshop on Theorem Proving Components for Educational Software, ThEdu@CADE 2019, Natal, Brazil, 25th August 2019.	ThEdu@CADE	2020	DBLP DOI BibTeX RDF
19	Adnan Rashid, Umair Siddique, Sofiène Tahar	Formal Verification of Cyber-Physical Systems using Theorem Proving (Invited Paper).	CoRR	2020	DBLP BibTeX RDF
19	Sa'ed Abed, Adnan Rashid, Osman Hasan	Formal Analysis of Unmanned Aerial Vehicles Using Higher-Order-Logic Theorem Proving.	J. Aerosp. Inf. Syst.	2020	DBLP DOI BibTeX RDF
19	Jan Jakubuv, Cezary Kaliszyk	Relaxed Weighted Path Order in Theorem Proving.	Math. Comput. Sci.	2020	DBLP DOI BibTeX RDF
19	Jasmin Blanchette, Sophie Tourret	Extensions to the Comprehensive Framework for Saturation Theorem Proving.	Arch. Formal Proofs	2020	DBLP BibTeX RDF
19	Sophie Tourret	A Comprehensive Framework for Saturation Theorem Proving.	Arch. Formal Proofs	2020	DBLP BibTeX RDF
19	Mnacho Echenim, Nicolas Peltier	Combining Induction and Saturation-Based Theorem Proving.	J. Autom. Reason.	2020	DBLP DOI BibTeX RDF
19	Jeremy Avigad, Assia Mahboubi	Preface: Selected Extended Papers from Interactive Theorem Proving 2018.	J. Autom. Reason.	2020	DBLP DOI BibTeX RDF
19	Ullrich Hustadt, Ana Ozaki, Clare Dixon	Theorem Proving for Pointwise Metric Temporal Logic Over the Naturals via Translations.	J. Autom. Reason.	2020	DBLP DOI BibTeX RDF
19	Stefan Mitsch, Jonathan Julián Huerta y Munive, Xiangyu Jin, Bohua Zhan, Shuling Wang, Naijun Zhan	ARCH-COMP20 Category Report: Hybrid Systems Theorem Proving.	ARCH	2020	DBLP DOI BibTeX RDF
19	Sa'ed Abed, Adnan Rashid, Osman Hasan	Formal analysis of the biological circuits using higher-order-logic theorem proving.	SAC	2020	DBLP DOI BibTeX RDF
19	Marianna Girlando, Björn Lellmann, Nicola Olivetti, Stefano Pesce, Gian Luca Pozzato	Theorem Proving for Lewis Logics of Counterfactual Reasoning.	CILC	2020	DBLP BibTeX RDF
19	Guangshuai Mo, Yan Xiong, Wenchao Huang, Lu Ma	Automated Theorem Proving via Interacting with Proof Assistants by Dynamic Strategies.	BigCom	2020	DBLP DOI BibTeX RDF
19	Chuanhu Cheng, Yan Xiong, Wenchao Huang, Lu Ma	Context-aware Generation of Proof Scripts for Theorem Proving.	BigCom	2020	DBLP DOI BibTeX RDF
19	Alexander V. Lyaletski, Alexandre Lyaletsky	Evidence Algorithm Approach to Automated Theorem Proving and SAD Systems.	IT&I	2020	DBLP BibTeX RDF
19	Agnieszka Slowik, Chaitanya Mangla, Mateja Jamnik, Sean B. Holden, Lawrence C. Paulson	Bayesian Optimisation for Premise Selection in Automated Theorem Proving (Student Abstract).	AAAI	2020	DBLP DOI BibTeX RDF
19	Aditya Paliwal, Sarah M. Loos, Markus N. Rabe, Kshitij Bansal, Christian Szegedy	Graph Representations for Higher-Order Logic and Theorem Proving.	AAAI	2020	DBLP DOI BibTeX RDF
19	Stephan Schulz 0001, Adam Pease	Teaching Automated Theorem Proving by Example: PyRes 1.2 - (System Description).	IJCAR (2)	2020	DBLP DOI BibTeX RDF
19	Bernhard Gleiss, Laura Kovács, Jakob Rath	Subsumption Demodulation in First-Order Theorem Proving.	IJCAR (1)	2020	DBLP DOI BibTeX RDF
19	Sebastian Ullrich 0002, Leonardo de Moura 0001	Beyond Notations: Hygienic Macro Expansion for Theorem Proving Languages.	IJCAR (2)	2020	DBLP DOI BibTeX RDF
19	Tiziano Dalmonte, Nicola Olivetti, Gian Luca Pozzato	HYPNO: Theorem Proving with Hypersequent Calculi for Non-normal Modal Logics (System Description).	IJCAR (2)	2020	DBLP DOI BibTeX RDF
19	Uwe Waldmann, Sophie Tourret, Simon Robillard, Jasmin Blanchette	A Comprehensive Framework for Saturation Theorem Proving.	IJCAR (1)	2020	DBLP DOI BibTeX RDF
19	Bernhard Gleiss, Martin Suda 0001	Layered Clause Selection for Saturation-Based Theorem Proving.	PAAR+SC²@IJCAR	2020	DBLP BibTeX RDF
19	Tiziano Dalmonte, Sara Negri, Nicola Olivetti, Gian Luca Pozzato	Theorem Proving for Non-normal Modal Logics.	OVERLAY	2020	DBLP BibTeX RDF
19	Yassmeen Elderhalli, Osman Hasan, Sofiène Tahar	A Framework for Formal Dynamic Dependability Analysis Using HOL Theorem Proving.	CICM	2020	DBLP DOI BibTeX RDF
19	Asta Halkjær From, Jørgen Villadsen, Patrick Blackburn	Isabelle/HOL as a Meta-Language for Teaching Logic.	ThEdu@IJCAR	2020	DBLP DOI BibTeX RDF
19	Walther Neuper	Lucas-Interpretation on Isabelle's Functions.	ThEdu@IJCAR	2020	DBLP DOI BibTeX RDF
19	Mauricio Ayala-Rincón, Thaynara Arielly de Lima	Teaching Interactive Proofs to Mathematicians.	ThEdu@IJCAR	2020	DBLP DOI BibTeX RDF
19	Merlin Carl	Number Theory and Axiomatic Geometry in the Diproche System.	ThEdu@IJCAR	2020	DBLP DOI BibTeX RDF
19	Filip Maric, Sana Stojanovic-Durdevic	Formalizing IMO Problems and Solutions in Isabelle/HOL.	ThEdu@IJCAR	2020	DBLP DOI BibTeX RDF
19	Geoff Sutcliffe	The CADE-27 Automated theorem proving System Competition - CASC-27.	AI Commun.	2019	DBLP DOI BibTeX RDF
19	Wilayat Khan, Muhammad Kamran, Aakash Ahmad, Farrukh Aslam Khan, Abdelouahid Derhab	Formal Analysis of Language-Based Android Security Using Theorem Proving Approach.	IEEE Access	2019	DBLP DOI BibTeX RDF
19	Yassmeen Elderhalli, Osman Hasan, Sofiène Tahar	A Methodology for the Formal Verification of Dynamic Fault Trees Using HOL Theorem Proving.	IEEE Access	2019	DBLP DOI BibTeX RDF
19	Yassmeen Elderhalli, Waqar Ahmad, Osman Hasan, Sofiène Tahar	Probabilistic Analysis of Dynamic Fault Trees using HOL Theorem Proving.	FLAP	2019	DBLP BibTeX RDF
19	Mladen Nikolic, Vesna Marinkovic, Zoltán Kovács, Predrag Janicic	Portfolio theorem proving and prover runtime prediction for geometry.	Ann. Math. Artif. Intell.	2019	DBLP DOI BibTeX RDF
19	Hongbo Li 0012	Automated Theorem Proving Practice with Null Geometric Algebra.	J. Syst. Sci. Complex.	2019	DBLP DOI BibTeX RDF
19	Bohua Zhan	holpy: Interactive Theorem Proving in Python.	CoRR	2019	DBLP BibTeX RDF
19	Naveen Sundar Govindarajulu, Selmer Bringsjord, Matthew Peveler	On Quantified Modal Theorem Proving for Modeling Ethics.	ARCADE@CADE	2019	DBLP DOI BibTeX RDF
19	Kshitij Bansal, Sarah M. Loos, Markus N. Rabe, Christian Szegedy, Stewart Wilcox	HOList: An Environment for Machine Learning of Higher-Order Theorem Proving (extended version).	CoRR	2019	DBLP BibTeX RDF
19	Yutaka Nagashima	Towards Evolutionary Theorem Proving for Isabelle/HOL.	CoRR	2019	DBLP BibTeX RDF
19	Aditya Paliwal, Sarah M. Loos, Markus N. Rabe, Kshitij Bansal, Christian Szegedy	Graph Representations for Higher-Order Logic and Theorem Proving.	CoRR	2019	DBLP BibTeX RDF
19	Sa'ed Abed, Adnan Rashid, Osman Hasan	Formal Analysis of the Biological Circuits using Higher-order-logic Theorem Proving.	CoRR	2019	DBLP BibTeX RDF
19	Giselle Reis, Haniel Barbosa (eds.)	Proceedings Sixth Workshop on Proof eXchange for Theorem Proving, PxTP 2019, Natal, Brazil, August 26, 2019.	PxTP	2019	DBLP DOI BibTeX RDF
19	Waqar Ahmed, Shahid Ali Murtza, Osman Hasan, Sofiène Tahar	On the Formalization of Importance Measures using HOL Theorem Proving.	CoRR	2019	DBLP BibTeX RDF
19	Bartosz Piotrowski, Josef Urban	Guiding Theorem Proving by Recurrent Neural Networks.	CoRR	2019	DBLP BibTeX RDF
19	Grzegorz Wiaderek, Iwona Skalna	Generating theorem proving procedures from axioms of Truncated Predicate Calculus.	CoRR	2019	DBLP BibTeX RDF
19	John Hester	Automated ZFC Theorem Proving with E.	CoRR	2019	DBLP BibTeX RDF
19	Pedro Quaresma, Walther Neuper (eds.)	Proceedings 7th International Workshop on Theorem proving components for Educational software, ThEdu@FLoC 2018, Oxford, United Kingdom, 18 july 2018.	ThEdu@FLoC	2019	DBLP DOI BibTeX RDF
19	Yassmeen Elderhalli, Osman Hasan, Sofiène Tahar	Dynamic Dependability Analysis of Shuffle-exchange Networks using HOL Theorem Proving.	CoRR	2019	DBLP BibTeX RDF
19	Glyn Morrill	Parsing/Theorem-Proving for Logical Grammar CatLog3.	J. Log. Lang. Inf.	2019	DBLP DOI BibTeX RDF
19	Alexander Steen	Higher-order theorem proving and its applications.	it Inf. Technol.	2019	DBLP DOI BibTeX RDF
19	Sophie Siebert, Claudia Schon, Frieder Stolzenburg	Commonsense Reasoning Using Theorem Proving and Machine Learning.	CD-MAKE	2019	DBLP DOI BibTeX RDF
19	Adnan Rashid, Umair Siddique, Sofiène Tahar	Formal Verification of Cyber-Physical Systems Using Theorem Proving.	FTSCS	2019	DBLP DOI BibTeX RDF
19	Diego Marmsoler	Verifying Dynamic Architectures using Model Checking and Interactive Theorem Proving.	SE/SWM	2019	DBLP DOI BibTeX RDF
19	Katrine Bjørn Pedersen Thoft, Nina Gierasimczuk	Cognitive Complexity of Logical Reasoning in Games: Automated Theorem Proving Perspective.	CogSci	2019	DBLP BibTeX RDF
19	Yutaka Nagashima	Towards evolutionary theorem proving for isabelle/HOL.	GECCO (Companion)	2019	DBLP DOI BibTeX RDF
19	Gabriel Ebner	Herbrand Constructivization for Automated Intuitionistic Theorem Proving.	TABLEAUX	2019	DBLP DOI BibTeX RDF
19	Kentaro Kikuchi, Takahito Aoto 0001, Isao Sasano	Inductive Theorem Proving in Non-terminating Rewriting Systems and Its Application to Program Transformation.	PPDP	2019	DBLP DOI BibTeX RDF
19	John Harrison 0001, John O'Leary, Andrew Tolmach (eds.)	10th International Conference on Interactive Theorem Proving, ITP 2019, September 9-12, 2019, Portland, OR, USA.	ITP	2019	DBLP BibTeX RDF