Search
Search Results
-
Formalizing the Independence of Propositional Logic Axiom System in Coq
The development of computer science has promoted the formalization of mathematical theorem proofs, making it especially crucial to use machine...
-
Making Higher-Order Superposition Work
Superposition is among the most successful calculi for first-order logic. Its extension to higher-order logic introduces new challenges such as...
-
Tableaux for Automated Reasoning in Dependently-Typed Higher-Order Logic
Dependent type theory gives an expressive type system facilitating succinct formalizations of mathematical concepts. In practice, it is mainly used...
-
Approximation Fixpoint Theory in Coq
Approximation Fixpoint Theory (AFT) is an abstract framework based on lattice theory that unifies semantics of different non-monotonic logic. AFT has...
-
MOIN: A Nested Sequent Theorem Prover for Intuitionistic Modal Logics (System Description)
We present a simple Prolog prover for intuitionistic modal logics based on nested sequent proof systems. We have implemented single-conclusion...
-
SAT-Based Subsumption Resolution
Subsumption resolution is an expensive but highly effective simplifying inference for first-order saturation theorem provers. We present a new...
-
Note on a Fibonacci parity sequence
Let ftm = 0111010010001⋯ be the analogue of the Thue-Morse sequence in Fibonacci representation. In this note we show how, using the
Walnut ...
-
A Heuristic Prover for Elementary Analysis in Theorema
We present a plug-in to the Theorema system, which generates proofs similar to those produced by humans for theorems in elementary analysis and is...
-
Formalizing Free Groups in Isabelle/HOL: The Nielsen-Schreier Theorem and the Conjugacy Problem
Free groups are central to group theory, and are ubiquitous across many branches of mathematics, including algebra, topology and geometry. An...
-
GeoLogic – Graphical Interactive Theorem Prover for Euclidean Geometry
Domain of mathematical logic in computers is dominated by automated theorem provers (ATP) and interactive theorem provers (ITP). Both of these are...
-
Synthesis of Recursive Programs in Saturation
We turn saturation-based theorem proving into an automated framework for recursive program synthesis. We introduce magic axioms as valid induction...
-
A Resolution-Based Interactive Proof System for UNSAT
Modern SAT or QBF solvers are expected to produce correctness certificates. However, certificates have worst-case exponential size (unless...
-
Program Synthesis in Saturation
We present an automated reasoning framework for synthesizing recursion-free programs using saturation-based theorem proving. Given a functional...
-
Regularization in Spider-Style Strategy Discovery and Schedule Construction
To achieve the best performance, automatic theorem provers often rely on schedules of diverse proving strategies to be tried out (either sequentially...
-
Formalization of Functional Block Diagrams Using HOL Theorem Proving
Functional Block Diagrams (FBD) are commonly used as a graphical representation for safety analysis in a wide range of complex engineering...
-
Formalizing Piecewise Affine Activation Functions of Neural Networks in Coq
Verification of neural networks relies on activation functions being piecewise affine (pwa)—enabling an encoding of the verification problem for...
-
Formal Reasoning Using Distributed Assertions
When a proof system checks a formal proof, we can say that its kernel asserts that the formula is a theorem in a particular logic. We describe a...
-
Single-to-Multi-theorem Transformations for Non-interactive Statistical Zero-Knowledge
Non-interactive zero-knowledge proofs or arguments allow a prover to show validity of a statement without further interaction. For non-trivial...
-
Approximate Lower Bound Arguments
Suppose a prover, in possession of a large body of valuable evidence, wants to quickly convince a verifier by presenting only a small portion of the...