Rob Arthan
Rob Arthan
This paper reports on a simpler and more powerful replacement for the principles for defining new constants that were previously provided in the various HOL implementations. We discuss the problems that the new principle is intended to solv...
Christoph Benzmüller,Nik Sultana,Lawrence C Paulson et al.
Christoph Benzmüller et al.
Leo-II is an automated theorem prover for classical higher-order logic. The prover has pioneered cooperative higher-order-first-order proof automation, it has influenced the development of the TPTP THF infrastructure for higher-order logic,...
Łukasz Czajka,Cezary Kaliszyk
Łukasz Czajka
Hammers provide most powerful general purpose automation for proof assistants based on HOL and set theory today. Despite the gaining popularity of the more advanced versions of type theory, such as those based on the Calculus of Inductive C...
A Verified SAT Solver Framework with Learn, Forget, Restart, and Incrementality [0.03%]
一个具有学习、遗忘、重启和增量性的已验证SAT求解器框架
Jasmin Christian Blanchette,Mathias Fleury,Peter Lammich et al.
Jasmin Christian Blanchette et al.
We developed a formal framework for conflict-driven clause learning (CDCL) using the Isabelle/HOL proof assistant. Through a chain of refinements, an abstract CDCL calculus is connected first to a more concrete calculus, then to a SAT solve...
Cornelius Diekmann,Lars Hupel,Julius Michaelis et al.
Cornelius Diekmann et al.
This article summarizes our efforts around the formally verified static analysis of iptables rulesets using Isabelle/HOL. We build our work around a formal semantics of the behavior of iptables firewalls. This semantics is tailored to the s...
Fabian Immler
Fabian Immler
A rigorous numerical algorithm, formally verified with Isabelle/HOL, is used to certify the computations that Tucker used to prove chaos for the Lorenz attractor. The verification is based on a formalization of a diverse variety of mathemat...
The Role of the Mizar Mathematical Library for Interactive Proof Development in Mizar [0.03%]
Mizar数学库在Mizar中进行交互式证明开发中的作用
Grzegorz Bancerek,Czesław Byliński,Adam Grabowski et al.
Grzegorz Bancerek et al.
The Mizar system is one of the pioneering systems aimed at supporting mathematical proof development on a computer that have laid the groundwork for and eventually have evolved into modern interactive proof assistants. We claim that an impo...
Nicolas Matentzoglu,Bijan Parsia,Uli Sattler
Nicolas Matentzoglu
Reasoning with SROIQ(D) , the logic that underpins the popular Web Ontology Language (OWL), has a high worst case complexity (N2Exptime). Decomposing the ontology into modules prior to classification, and then classifying the composites one...
Genetic Programming [Formula: see text] Proof Search [Formula: see text] Automatic Improvement [0.03%]
遗传编程[公式]证明搜索[公式]自动改进
Zoltan A Kocsis,Jerry Swan
Zoltan A Kocsis
Search Based Software Engineering techniques are emerging as important tools for software maintenance. Foremost among these is Genetic Improvement, which has historically applied the stochastic techniques of Genetic Programming to optimize ...
Bijan Parsia,Nicolas Matentzoglu,Rafael S Gonçalves et al.
Bijan Parsia et al.
The OWL Reasoner Evaluation competition is an annual competition (with an associated workshop) that pits OWL 2 compliant reasoners against each other on various standard reasoning tasks over naturally occurring problems. The 2015 competitio...