Keyword:higher-order logic

Publications
Formalization of Transform Methods in Higher-Order Logic: a Survey Muhammad Ahmed and Adnan Rashid EasyChair Preprint 8009
Formalization of RBD-based Cause Consequence Analysis in HOL Mohamed Abdelghany and Sofiene Tahar EasyChair Preprint 5720
Building Blocks for Reasoning on the BEAM Johannes Schuster and Christoph Benzmüller In:Proceedings of 16th International Workshop on the Implementation on Logics. Proceedings of the 26th Conference on Logic for Programming, Artificial Intelligence, and Reasoning (short papers)
Experiments on Automating Boolos' Curious Inference Alexander Steen and Melanie Taprogge In:Proceedings of the 26th Conference on Logic for Programming, Artificial Intelligence, and Reasoning
Formal Verification of Proofs from Automated Theorem Provers for Higher-Order Logic Melanie Taprogge, Frédéric Blanqui and Alexander Steen In:Proceedings of the 26th Conference on Logic for Programming, Artificial Intelligence, and Reasoning
Aligning HOL-Light and Rocq Libraries Formally Frédéric Blanqui and Antoine Gontard In:Proceedings of the 26th Conference on Logic for Programming, Artificial Intelligence, and Reasoning
Translating HOL-Light proofs to Coq Frédéric Blanqui In:Proceedings of 25th Conference on Logic for Programming, Artificial Intelligence and Reasoning
A Mechanised Semantics for HOL with Ad-hoc Overloading Johannes Åman Pohjola and Arve Gengelbach In:LPAR23. LPAR-23: 23rd International Conference on Logic for Programming, Artificial Intelligence and Reasoning
Towards Strong Higher-Order Automation for Fast Interactive Verification Jasmin Christian Blanchette, Pascal Fontaine, Stephan Schulz and Uwe Waldmann In:ARCADE 2017. 1st International Workshop on Automated Reasoning: Challenges, Applications, Directions, Exemplary Achievements
Leo-III Version 1.1 (System description) Christoph Benzmüller, Alexander Steen and Max Wisniewski In:IWIL Workshop and LPAR Short Presentations
TacticToe: Learning to Reason with HOL4 Tactics Thibault Gauthier, Cezary Kaliszyk and Josef Urban In:LPAR-21. 21st International Conference on Logic for Programming, Artificial Intelligence and Reasoning
Theorem Provers For Every Normal Modal Logic Tobias Gleißner, Alexander Steen and Christoph Benzmüller In:LPAR-21. 21st International Conference on Logic for Programming, Artificial Intelligence and Reasoning
Towards Formal Reliability Analysis of Logistics Service Supply Chains using Theorem Proving Waqar Ahmed, Osman Hasan and Sofiene Tahar In:IWIL-2015. 11th International Workshop on the Implementation of Logics
Embedding of Quantified Higher-Order Nominal Modal Logic into Classical Higher-Order Logic Max Wisniewski and Alexander Steen In:ARQNL 2014. Automated Reasoning in Quantified Non-Classical Logics
Understanding LEO-II’s proofs Nik Sultana and Christoph Benzmüller In:IWIL 2012. The 9th International Workshop on the Implementation of Logics
External Tools for the Formal Proof of the Kepler Conjecture Thomas C. Hales In:PxTP 2013. Third International Workshop on Proof Exchange for Theorem Proving
Stronger Automation for Flyspeck by Feature Weighting and Strategy Evolution Cezary Kaliszyk and Josef Urban In:PxTP 2013. Third International Workshop on Proof Exchange for Theorem Proving
Challenges in Using OpenTheory to Transport Harrison's HOL Model from HOL Light to HOL4 Ramana Kumar In:PxTP 2013. Third International Workshop on Proof Exchange for Theorem Proving
Initial Experiments on Deriving a Complete HOL Simplification Set Cezary Kaliszyk and Thomas Sternagel In:PxTP 2013. Third International Workshop on Proof Exchange for Theorem Proving
From Classical Extensional Higher-Order Tableau to Intuitionistic Intentional Natural Deduction Chad E. Brown and Christine Rizkallah In:PxTP 2013. Third International Workshop on Proof Exchange for Theorem Proving
Robust, Semi-Intelligible Isabelle Proofs from ATP Proofs Steffen Juilf Smolka and Jasmin Christian Blanchette In:PxTP 2013. Third International Workshop on Proof Exchange for Theorem Proving
LEO-II Version 1.5 Christoph Benzmüller and Nik Sultana In:PxTP 2013. Third International Workshop on Proof Exchange for Theorem Proving
Nitpick: A Counterexample Generator for Isabelle/HOL Based on the Relational Model Finder Kodkod Jasmin Christian Blanchette In:LPAR-17-short. short papers for 17th International Conference on Logic for Programming, Artificial intelligence, and Reasoning.
Composable Packages for Higher Order Logic Theories Joe Hurd In:VERIFY-2010. 6th International Verification Workshop