scientific article; zbMATH DE number 7761008

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.

zbMATH Keywords

sequent calculusnatural deductionresolutionproof systemsformalization of logic

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35)

Related Items (5)

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

This page was built for publication: