Formalization of the resolution calculus for first-order logic
From MaRDI portal
(Redirected from Publication:1663242)
Recommendations
- Formalization of the Resolution Calculus for First-Order Logic
- Formalizing Bachmair and Ganzinger's ordered resolution prover
- Formalizing Bachmair and Ganzinger's ordered resolution prover
- A full formalization of SLD-resolution in the calculus of inductive constructions
- Theorem Proving in Higher Order Logics
Cites work
- scientific article; zbMATH DE number 5539366 (Why is no real title available?)
- scientific article; zbMATH DE number 4072439 (Why is no real title available?)
- scientific article; zbMATH DE number 1301853 (Why is no real title available?)
- scientific article; zbMATH DE number 612169 (Why is no real title available?)
- scientific article; zbMATH DE number 976360 (Why is no real title available?)
- scientific article; zbMATH DE number 837700 (Why is no real title available?)
- scientific article; zbMATH DE number 3310921 (Why is no real title available?)
- scientific article; zbMATH DE number 3415409 (Why is no real title available?)
- A Linear Format for Resolution With Merging and a New Technique for Establishing Completeness
- A Machine-Oriented Logic Based on the Resolution Principle
- A machine-assisted proof of Gödel's incompleteness theorems for the theory of hereditarily finite sets
- A mechanised proof of Gödel's incompleteness theorems using Nominal Isabelle
- A transfinite Knuth-Bendix order for lambda-free higher-order terms
- A verified SAT solver framework with learn, forget, restart, and incrementality
- Concrete semantics. With Isabelle/HOL
- Deductive synthesis of the unification algorithm
- Efficient verified (UN)SAT certificate checking
- Extending Sledgehammer with SMT solvers
- Formal correctness of a quadratic unification algorithm
- Formalization of the Resolution Calculus for First-Order Logic
- Formalizing Bachmair and Ganzinger's ordered resolution prover
- Formalizing Knuth-Bendix orders and Knuth-Bendix completion
- Foundational extensible corecursion: a proof assistant perspective
- Isabelle/HOL. A proof assistant for higher-order logic
- Kripke models for classical logic
- Mathematical Logic for Computer Science
- Metamathematics, Machines and Gödel's Proof
- On Different Concepts of Resolution
- Partial and nested recursive function definitions in higher-order logic
- Self-formalisation of higher-order logic. Semantics, soundness, and a verified implementation
- Soundness and completeness proofs by coinductive methods
- System description: E 1.8
- Term Rewriting and All That
- Term indexing
- The Gödel completeness theorem for uncountable languages
- The blossom of finite semantic trees
- The reflective Milawa theorem prover is sound (down to the machine code that runs it)
- Theorem Proving in Higher Order Logics
- Towards Self-verification of HOL Light
- Truly modular (co)datatypes for Isabelle/HOL
- Unified Classical Logic Completeness
- Verifying the unification algorithm in LCF
- Visual theorem proving with the Incredible Proof Machine
Cited in
(12)- scientific article; zbMATH DE number 7649968 (Why is no real title available?)
- Verifying a sequent calculus Prover for first-order logic with functions in Isabelle/HOL
- scientific article; zbMATH DE number 7561490 (Why is no real title available?)
- Conflict resolution: a first-order resolution calculus with decision literals and conflict-driven clause learning
- Formalizing Bachmair and Ganzinger's ordered resolution prover
- Formalization of the Resolution Calculus for First-Order Logic
- A full formalization of SLD-resolution in the calculus of inductive constructions
- Formalizing Bachmair and Ganzinger's ordered resolution prover
- On structures of regular standard contradictions in propositional logic
- Formalized proof systems for propositional logic
- scientific article; zbMATH DE number 5173934 (Why is no real title available?)
- Verified Decision Procedures for Modal Logics.
Describes a project that uses
Uses Software
- Isabelle
- Isabelle/HOL
- SPASS
- Isar
- Sledgehammer
- LCF
- Milawa
- E Theorem Prover
- Jitawa
- IsaFoL
- theoremprover-museum
- GRAT
- Completeness theorem
- Superposition Calculus
- Paraconsistency
- Knuth Bendix Orders
- Abstract Completeness
- FOL Fitting
- Incompleteness Theorems
- Archive Formal Proofs
- Lambda Free RPOs
- Verified Prover
- Abstract Soundness
- Incredible Proof Machine
- Propositional Resolution
- FOL_Harrison
- GitHub
This page was built for publication: Formalization of the resolution calculus for first-order logic
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q1663242)
