The role of first-order theorem proving as a core theme of automated deduction was recognized since the beginning of the field, at the dawn of Artificial Intelligence, more than forty years ago. Although many other logics have been developed and used in AI, deduction systems based on first-order theorem proving recently have achieved considerable successes and even mention in the general press. It was a first-order theorem prover that first proved the Robbins algebra conjecture, and thus reached the New York Times Science section (NY Times, Dec. 10, 1996).
Special issue on advances in first-order theorem proving - Foreword of the guest editors
Bonacina, MP;
2000-01-01
Abstract
The role of first-order theorem proving as a core theme of automated deduction was recognized since the beginning of the field, at the dawn of Artificial Intelligence, more than forty years ago. Although many other logics have been developed and used in AI, deduction systems based on first-order theorem proving recently have achieved considerable successes and even mention in the general press. It was a first-order theorem prover that first proved the Robbins algebra conjecture, and thus reached the New York Times Science section (NY Times, Dec. 10, 1996).
File 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.
