A Programming Notation for Tactical Reasoning
A notation for expressing the control algorithms (subgoaling strategies) of natural deduction theorem provers is presented. The language provides tools for building widely known, fundamental theorem proving strategies and is independent of the problem area and inference rule system chosen, facilitating formulation of high level algorithms that can be compared, analyzed, and even ported across theorem proving systems. The notation is a simplification and generalization of the tactic language of Edinburgh LCF. Examples using a natural deduction system for propositional logic are given.
KeywordsInference Rule Propositional Logic Theorem Prove Natural Deduction Rule Scheme
Unable to display preview. Download preview PDF.
- (And).Andrews, P.B. Transformaing matings into natural deduction proofs. 5th Conference on Automated Deduction, Les Arcs, France, 1980, LNCS 87, pp. 281–292.Google Scholar
- (Ble).Bledsoe, W.W., and Tyson, M. The UT interactive theorem prover. Memo ATP-17, Mathematics Dept., University of Texas, Austin, 1975.Google Scholar
- (Coh).Cohen, P.R., and Feigenbaum, E.A., eds. The Handbook of Artificial Intelligence, Vol. 3. Pittman, New York, Ch. 12.Google Scholar
- (Con).Cohn, A. The equivalence of two semantic definitions: a case study in LCF. Report CSR-76-81, Computer Science Dept., University of Edinburgh, Scotland, 1981.Google Scholar
- (CoM).Cohn, A., and Milner, R. On using Edinburgh LCF to prove the correctness of a parsing algorithm. Report CSR-113-82, Computer Science Dept., University of Edinburgh, Scotland, 1982.Google Scholar
- (Gut).Guttag, J. Notes on type abstraction. IEEE Trans. on Software Engg. SE-6-1 (1980) 13–23.Google Scholar
- (Les).Leszczyłowski, J. An experiment with Edinburgh LCF. 5th Conference on Automated Deduction, Les Arcs, France, 1980, LNCS 87, pp. 170–181.Google Scholar
- (Mon).Monahan, B. Ph.D. thesis, University of Edinburgh, forthcoming.Google Scholar
- (Nor).Nordström, B. Programming in constructive set theory: some examples. ACM Conf. on Functional Programming Languages and Computer Architecture, Portsmouth, N.H., 1981, pp. 141–153.Google Scholar
- (Plo).Plotkin, G. A structural approach to operational semantics. Report DAIMI FN-19, Computer Science Dept., University of Aarhus, Denmark, 1981.Google Scholar
- (Rob).Robinson, J.A. Logic:Form and Function. Edinburgh Univ. Press, Edinburgh, 1979.Google Scholar