Automated deduction in von Neumann-Bernays-Gödel set theory
From MaRDI portal
Publication:1187858
DOI10.1007/BF00263451zbMath0768.03005OpenAlexW2041161966MaRDI QIDQ1187858
Publication date: 23 July 1992
Published in: Journal of Automated Reasoning (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1007/bf00263451
heuristicsclausal version of Neumann-Bernays-Gödel axiomatization of set theoryresolution-based automated theorem prover Otter
Mechanization of proofs and logical operations (03B35) Nonclassical and second-order set theories (03E70)
Related Items
Issues in commonsense set theory ⋮ The TPTP problem library and associated infrastructure and associated infrastructure. The FOF and CNF parts, v3.5.0 ⋮ The Relative Consistency of the Axiom of Choice — Mechanized Using Isabelle/ZF ⋮ The TPTP problem library and associated infrastructure. From CNF to TH0, TPTP v6.4.0 ⋮ Computer proofs about finite and regular sets: The unifying concept of subvariance. ⋮ Theorem Proving in Large Formal Mathematics as an Emerging AI Field ⋮ MBase: Representing knowledge and context for the integration of mathematical software systems ⋮ The TPTP problem library ⋮ Set theory for verification. I: From foundations to functions ⋮ Set graphs. III: Proof pearl: Claw-free graphs mirrored into transitive hereditarily finite sets
This page was built for publication: Automated deduction in von Neumann-Bernays-Gödel set theory
