×

Inference rules using local contexts. (English) Zbl 0715.03006

Summary: We construct equivalent “localized” versions of a formula, adding assumptions simultaneously to various locations, where the particular location determines what is added. Inference rules that take advantage of localized formulas are presented for sequent calculi in which the left hand side of sequents can be used to accumulate the background assumptions (or “contexts”) of assertions. The intended application is to the automatic generation of tractable justifying lemmas for substitution operations for interactive proof development systems, especially those concerned with mathematical topics where manipulation of deeply embedded terms is desirable.

MSC:

03B35 Mechanization of proofs and logical operations
68T15 Theorem proving (deduction, resolution, etc.) (MSC2010)

Software:

Automath
PDFBibTeX XMLCite
Full Text: DOI

References:

[1] Bell, J. and Machover, M., A Course in Mathematical Logic, North-Holland, New York, N.Y. (1977). · Zbl 0359.02001
[2] deBruijn, N. J., ?The mathematical language AUTOMATH, its usage, and some of its extensions?, in Symposium on Automatic Demonstration, Lecture Notes in Mathematics, vol. 125, Springer-Verlag, Berlin (1970).
[3] Robinson, J. A., Logic: Form and Function, Artificial Intelligence Series, North-Holland, New York, N.Y. (1979).
[4] Schoenfield, J., Mathematical Logic, Addison-Wesley, Reading, Mass. (1967).
[5] Schutte, K., Proof Theory, trans. J. N. Crossley, Springer-Verlag, Berlin (1977).
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.