The SAD System: Deductive Assistance in an Intelligent Linguistic Environment

Formal methods are widely used in the computer science community. Formal verification and certification is an important component of any formal approach. Such a work can not be done by hand, hence the software that can do a part of it is rather required. The verification methods are often based on a deductive system and "verify" means "prove". Corresponding software is called proof assistant. We describe in this paper the System for Automated Deduction (SAD): its architecture, input language, and reasoning facilities. We show how to use SAD as a proof assistant. We outline specific features of SAD - a handy input language, powerful reasoning strategy, opportunity to use various low level inference engines. Examples and results of some experiments are also given