The goal of this paper is to present a formal system FB for bidirectional realoning which integrates forward and backward deduction. FB is proved equivalent to Gentzen's classical system of propositional naturla deduction. FB is the logic od a theorem prover which supports interactive proof construction in general domains
Bidirectional Reasoning
Agostini, Alessandro;Giunchiglia, Fausto
1995-01-01
Abstract
The goal of this paper is to present a formal system FB for bidirectional realoning which integrates forward and backward deduction. FB is proved equivalent to Gentzen's classical system of propositional naturla deduction. FB is the logic od a theorem prover which supports interactive proof construction in general domainsFile in questo prodotto:
Non ci sono file associati a questo prodotto.
I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.
