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 (18)

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

This page was built for publication: Set theory in first-order logic: Clauses for Gödel's axioms