This Article 
   
 Share 
   
 Bibliographic References 
   
 Add to: 
 
Digg
Furl
Spurl
Blink
Simpy
Google
Del.icio.us
Y!MyWeb
 
 Search 
   
A Semantically Guided Deductive System for Automatic Theorem Proving
April 1976 (vol. 25 no. 4)
pp. 328-334
ASCII Text
x 
 
R. Reiter, "A Semantically Guided Deductive System for Automatic Theorem Proving," IEEE Transactions on Computers, vol. 25, no. 4, pp. 328-334, April, 1976.
 
 
BibTex
x
 
@article{ 10.1109/TC.1976.1674613,
author = {R. Reiter},
title = {A Semantically Guided Deductive System for Automatic Theorem Proving},
journal ={IEEE Transactions on Computers},
volume = {25},
number = {4},
issn = {0018-9340},
year = {1976},
pages = {328-334},
doi = {http://doi.ieeecomputersociety.org/10.1109/TC.1976.1674613},
publisher = {IEEE Computer Society},
address = {Los Alamitos, CA, USA},
}
 
 
RefWorks Procite/RefMan/Endnote
x 
 
TY - JOUR
JO - IEEE Transactions on Computers
TI - A Semantically Guided Deductive System for Automatic Theorem Proving
IS - 4
SN - 0018-9340
SP328
EP334
EPD - 328-334
A1 - R. Reiter,
PY - 1976
KW - Natural deduction
KW - semantics
KW - theorem proving.
VL - 25
JA - IEEE Transactions on Computers
ER -
 
R. Reiter, Department of Computer Science, University ty of British Columbia
A semantic and deductive formal system for automatic theorem proving is presented. The system has, as its deductive component, a form of natural deduction. Its semantic component relies on an underlying representation of a model. This model is invoked to prune subgoals generated by the deductive component, whenever such subgoals test false in the model. In addition, the model is used to suggest inferences to be made at the deductive level. Conversely, the current state of the proof suggests changes to be made to the model, e.g., when a construction is required as in geometry.
Index Terms:
Natural deduction, semantics, theorem proving.
Citation:
R. Reiter, "A Semantically Guided Deductive System for Automatic Theorem Proving," IEEE Transactions on Computers, vol. 25, no. 4, pp. 328-334, April 1976, doi:10.1109/TC.1976.1674613
Usage of this product signifies your acceptance of the Terms of Use.