scientific article; zbMATH DE number 1301853
From MaRDI portal
Publication:4247076
zbMath0930.03010MaRDI QIDQ4247076
No author found.
Publication date: 15 February 2000
Title: zbMATH Open Web Interface contents unavailable due to conflicting licenses.
validitysemanticssatisfiabilitysyntaxUniformitySkolemizationCompactnessLöwenheim-SkolemHOL Light theorem provercanonical term modelsHOL datatypeunsorted first-order logic
Mechanization of proofs and logical operations (03B35) Basic properties of first-order languages and structures (03C07)
Related Items (10)
Soundness and completeness proofs by coinductive methods ⋮ A verified SAT solver framework with learn, forget, restart, and incrementality ⋮ Formalization of the resolution calculus for first-order logic ⋮ Hall's theorem for enumerable families of finite sets ⋮ Unnamed Item ⋮ A Verified SAT Solver Framework with Learn, Forget, Restart, and Incrementality ⋮ A Verified Runtime for a Verified Theorem Prover ⋮ Formalization of the Resolution Calculus for First-Order Logic ⋮ Mechanised modal model theory ⋮ Formally verified tableau-based reasoners for a description logic
Uses Software
This page was built for publication:
