Abstract
In an oversimplified and abstract view, given a logic (syntax, semantics, inference system) L and a knowledge base K of formulae in L.
-
“computer” for K enables the user to provide an expression (term, formula, program) T with a free variable x and a value υ (from an appropriate domain) and “evaluates” T x←υ (T with υ substituted for x) w.r.t. K in L.
-
“solver” for K enables the user to provide an expression T with a free variable x and produces (all) values υ for which T x←υ holds w.r.t. K in L, and
-
“prover” for K enables the user to provide an expression T with a free variable x and generates a proof (or disproves) that, for all values υ, T x←υ holds w.r.t. K in L.
This is a preview of subscription content, log in via an institution.
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1997 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Buchberger, B. (1997). Computing, solving, proving: A report on the Theorema project. In: Dix, J., Furbach, U., Nerode, A. (eds) Logic Programming And Nonmonotonic Reasoning. LPNMR 1997. Lecture Notes in Computer Science, vol 1265. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-63255-7_16
Download citation
DOI: https://doi.org/10.1007/3-540-63255-7_16
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-63255-9
Online ISBN: 978-3-540-69249-2
eBook Packages: Springer Book Archive