Home | Quick Search | Advanced Search | Bibliography submission | Bibliography submission using bibtex | Bibliography submission using bibtex file | Links | Help | Internal

Details:

   
TitleAn automated prover for Zermelo–Fraenkel set theory in Theorema
Author(s) Wolfgang Windsteiger
TypeArticle in Journal
AbstractThis paper presents some fundamental aspects of the design and the implementation of an automated prover for Zermelo–Fraenkel set theory within the Theorema system. The method applies the “Prove–Compute–Solve” paradigm as its major strategy for generating proofs in a natural style for statements involving constructs from set theory.
KeywordsAutomated theorem proving, Set theory, Theorema
ISSN0747-7171
URL http://www.sciencedirect.com/science/article/pii/S0747717105001495
LanguageEnglish
JournalJournal of Symbolic Computation
Volume41
Number3–4
Pages435 - 470
Year2006
NoteLogic, Mathematics and Computer Science: Interactions in honor of Bruno Buchberger (60th birthday)
Edition0
Translation No
Refereed No
Webmaster