Automated deduction in von Neumann-Bernays-Gödel set theory
From MaRDI portal
Publication:1187858
DOI10.1007/BF00263451zbMath0768.03005MaRDI 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
heuristics; clausal version of Neumann-Bernays-Gödel axiomatization of set theory; resolution-based automated theorem prover Otter
03B35: Mechanization of proofs and logical operations
03E70: Nonclassical and second-order set theories
Related Items
Theorem Proving in Large Formal Mathematics as an Emerging AI Field, The TPTP problem library, MBase: Representing knowledge and context for the integration of mathematical software systems, Set theory for verification. I: From foundations to functions, Issues in commonsense set theory, Computer proofs about finite and regular sets: The unifying concept of subvariance., The TPTP problem library and associated infrastructure. From CNF to TH0, TPTP v6.4.0, Set graphs. III: Proof pearl: Claw-free graphs mirrored into transitive hereditarily finite sets, 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
