scientific article; zbMATH DE number 7761008
From MaRDI portal
DOI10.4230/lipics.types.2017.5zbMath1528.03097MaRDI QIDQ6060676
Tobias Nipkow, Julius Michaelis
Publication date: 3 November 2023
Title: zbMATH Open Web Interface contents unavailable due to conflicting licenses.
Related Items
Formalizing axiomatic systems for propositional logic in Isabelle/HOL, Verifying the conversion into CNF in dafny, Constructive and mechanised meta-theory of intuitionistic epistemic logic, Mechanising Gödel-Löb provability logic in HOL light, Hall's theorem for enumerable families of finite sets
Cites Work
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- A mechanised proof of Gödel's incompleteness theorems using Nominal Isabelle
- Self-formalisation of higher-order logic. Semantics, soundness, and a verified implementation
- Completeness and decidability results for CTL in constructive type theory
- Linear quantifier elimination
- Formalization and implementation of modern SAT solvers
- Isabelle/HOL. A proof assistant for higher-order logic
- A verified SAT solver framework with learn, forget, restart, and incrementality
- Formalization of the resolution calculus for first-order logic
- Formalized meta-theory of sequent calculi for substructural logics
- Structural cut elimination. I: Intuitionistic and classical logic
- Schlussweisen-Kalküle der Prädikatenlogik
- A Verified SAT Solver Framework with Learn, Forget, Restart, and Incrementality
- Formalization of the Resolution Calculus for First-Order Logic
- The Gödel Completeness Theorem for Uncountable Languages
- versat: A Verified Modern SAT Solver
- Concrete Semantics
- Certification of Termination Proofs Using CeTA
- Unified Classical Logic Completeness
- Inductive Beluga: Programming Proofs
- Revisiting Cut-Elimination: One Difficult Proof Is Really a Proof
- Towards Self-verification of HOL Light
- Metamathematics, Machines and Gödel's Proof
- Logic in Computer Science
- The Mechanical Verification of a DPLL-Based Satisfiability Solver
- Extending Sledgehammer with SMT Solvers
- Theorem Proving in Higher Order Logics
- Mechanising a Proof of Craig’s Interpolation Theorem for Intuitionistic Logic in Nominal Isabelle
- A UNIFYING PRINCIPAL IN QUANTIFICATION THEORY
- Partiality and recursion in interactive theorem provers – an overview
- Logic for computer scientists
