Techniques of computable set theory with applications to proof verification

DOI10.1002/cpa.3160480902zbMath0852.03004OpenAlexW2070159660MaRDI QIDQ4884662

Domenico Cantone, Alfredo Ferro

Publication date: 5 December 1996

Published in: Communications on Pure and Applied Mathematics (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1002/cpa.3160480902

zbMATH Keywords

surveytableau calculusdecision procedurefragments of set theorydecidability of satisfiabilitytopological closure operatorelementary graph theorymulti-sorted fragmentsproof verifier ETNA

Mathematics Subject Classification ID

Decidability of theories and sets of sentences (03B25) Mechanization of proofs and logical operations (03B35) Set theory (03E99)

Related Items (3)

A fast saturation strategy for set-theoretic tableaux ⋮ The decision problem for a three-sorted fragment of set theory with restricted quantification and finite enumerations ⋮ A tableau-based decision procedure for a fragment of set theory with iterated membership

Uses Software

• ISETL

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item

This page was built for publication: Techniques of computable set theory with applications to proof verification