Title | **An automated prover for Zermelo–Fraenkel set theory in Theorema** |

Author(s) | Wolfgang Windsteiger |

Type | Article in Journal |

Abstract | This 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. |

Keywords | Automated theorem proving, Set theory, Theorema |

ISSN | 0747-7171 |

URL |
http://www.sciencedirect.com/science/article/pii/S0747717105001495 |

Language | English |

Journal | Journal of Symbolic Computation |

Volume | 41 |

Number | 3–4 |

Pages | 435 - 470 |

Year | 2006 |

Note | Logic, Mathematics and Computer Science: Interactions in honor of Bruno Buchberger (60th birthday) |

Edition | 0 |

Translation |
No |

Refereed |
No |