Rechercher une page de manuel

Chercher une autre page de manuel:

dfg2otter

Langue: en

Version: 2003-04-29 (debian - 07/07/09)

Section: 1 (Commandes utilisateur)

NAME

dfg2otter - transforms DFG clause files into Otter format

SYNOPSIS

dfg2otter [options] <infile> <outfile>

DESCRIPTION

dfg2otter is a C-program to transform problem input files in DFG syntax into Otter syntax. It accepts all options from SPASS, although only a subset has an effect on translation.

dfg2otter negates conjecture formulae of the SPASS input file before printing the Otter usable list. The SPASS conjecture formula list is translated into a disjunction of the negated single conjectures. If the SPASS input file consits of clauses, these are not modified.

SEE ALSO

checkstat(1), filestat(1), pcs(1), pgen(1), rescmp(1), tpform(1), tpget(1), deprose(1), dfg2otter.pl(1), SPASS(1)

AUTHORS

Thomas Hillenbrand, Dalibor Topic and Christoph Weidenbach

Contact : Thomas Hillenbrand <hillen@mpi-sb.mpg.de>
          Christoph Weidenbach <weidenb@mpi-sb.mpg.de>

Puisque vous étudiez la géométrie et la trigonométrie, je vais vous
soumettre un problème :
Un bateau vogue sur l'Océan. Il a quitté Boston avec un chargement de
laine. Il jauge 200 tonneaux. Il se dirige vers le Havre. Le grand mat
est cassé, le garçon de cabine est sur le pont, il y a douze passagers
à bord. Le vent souffle E.N.-E. L'horloge marque 3 h 1/4. On est au mois
de mai. Quel est l'âge du capitaine ?
-+- Gustave Flaubert, lettre à sa soeur Caroline 1843 -+-