Set theory in first-order logic: Clauses for Gödel's axioms

DOI10.1007/BF02328452zbMath0635.03008OpenAlexW1966945932WikidataQ114264489 ScholiaQ114264489MaRDI QIDQ1097252

B. George

Publication date: 1986

Published in: Journal of Automated Reasoning (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/bf02328452

zbMATH Keywords

number theoryGödel's formulation of set theoryresolution-based automated theorem provingset of clauses for set theory

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35) Set theory (03E99)

Related Items

Issues in commonsense set theory ⋮ A finitely axiomatized formalization of predicate calculus with equality ⋮ The TPTP problem library and associated infrastructure and associated infrastructure. The FOF and CNF parts, v3.5.0 ⋮ ILF-SETHEO ⋮ TPS: A theorem-proving system for classical type theory ⋮ Computer proofs about finite and regular sets: The unifying concept of subvariance. ⋮ On sets, types, fixed points, and checkerboards ⋮ The problem of demodulating across argument and literal boundaries ⋮ Applying Light-Weight Theorem Proving to Debugging and Verifying Pointer Programs ⋮ Layered map reasoning ⋮ The TPTP problem library ⋮ Term rewriting: Some experimental results ⋮ The application of automated reasoning to formal models of combinatorial optimization ⋮ The kernel strategy and its use for the study of combinatory logic ⋮ Experimenting with Isabelle in ZF set theory ⋮ Set theory for verification. I: From foundations to functions ⋮ Set graphs. III: Proof pearl: Claw-free graphs mirrored into transitive hereditarily finite sets ⋮ A derived algorithm for evaluating \(\varepsilon\)-expressions over abstract sets

Cites Work

• Splitting and reduction heuristics in automatic theorem proving
• Unnamed Item
• Unnamed Item
• Unnamed Item