On sets, types, fixed points, and checkerboards

DOI10.1007/3-540-61208-4_1zbMath1415.03012OpenAlexW1576127349MaRDI QIDQ4645222

Matthew Bishop, Peter B. Andrews

Publication date: 10 January 2019

Published in: Theorem Proving with Analytic Tableaux and Related Methods (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/3-540-61208-4_1

zbMATH Keywords

automated reasoningtype theoryautomated theorem provingproof treeorder binary decision diagram

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35)

Related Items

Higher-Order Modal Logics: Automation and Applications

Uses Software

• TPS
• Mizar
• ETPS

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Set theory in first-order logic: Clauses for Gödel's axioms
• Bounds for proof-search and speed-up in the predicate calculus
• On Gödel's theorems on lengths of proofs I: Number of lines and speedup for arithmetics
• An interactive solution to the n x n mutilated checkerboard problem
• Ordered Binary Decision Diagrams and the Davis-Putnam procedure
• A formulation of the simple theory of types
• Consistency of the Continuum Hypothesis. (AM-3)

This page was built for publication: On sets, types, fixed points, and checkerboards