$next$ $up$ $previous$ $contents$
Next: Contents Contents

The Saturate System

Harald Ganzinger

Robert Nieuwenhuis

Pilar Nivela

Abstract:

The Saturate system is an experimental theorem prover for first-order logic, primarily based on saturation. Saturate uses techniques of ordered chaining for arbitrary transitive relations, including orderings, equivalence relations and congruences, and integrates CNF transformation lazily into saturation.

Contents
Installation
- Copying the System
- Installing the System
Overview
Getting started
Formula Syntax
- Context-free Syntax for Clauses.
The Interaction Cycle
Saturate Commands
Heuristics for the Definition of Meta-Logical Directives
Bibliography
Release Notes
Known Bugs
About this document ...

Harald Ganzinger 2002-12-04

Imprint | Data Protection