Hostname: page-component-78c5997874-4rdpn Total loading time: 0 Render date: 2024-11-16T15:20:47.077Z Has data issue: false hasContentIssue false

What is an inference rule?

Published online by Cambridge University Press:  12 March 2014

Ronald Fagin
Affiliation:
IBM Almaden Research Center, San Jose, California 95120-6099, E-mail: [email protected]
Joseph Y. Halpern
Affiliation:
IBM Almaden Research Center, San Jose, California 95120-6099, E-mail: [email protected]
Moshe Y. Vardi
Affiliation:
IBM Almaden Research Center, San Jose, California 95120-6099, E-mail: [email protected]

Abstract

What is an inference rule? This question does not have a unique answer. One usually finds two distinct standard answers in the literature; validity inference (σ ⊦vφ for every substitution τ, the validity of τ[σ] entails the validity of τ[φ]), and truth inference (σ⊦l φ if for every substitution τ, the truth of τ[σ] entails the truth of τ[φ]). In this paper we introduce a general semantic framework that allows us to investigate the notion of inference more carefully. Validity inference and truth inference are in some sense the extremal points in our framework. We investigate the relationship between various types of inference in our general framework, and consider the complexity of deciding if an inference rule is sound, in the context of a number of logics of interest: classical propositional logic, a nonstandard propositional logic, various propositional modal logics, and first-order logic.

Type
Research Article
Copyright
Copyright © Association for Symbolic Logic 1992

Access options

Get access to the full version of this content by using one of the access options below. (Log in options will check for institutional or personal access. Content may require purchase if you do not have access.)

References

REFERENCES

[AB75]Anderson, A. and Belnap, N. D., Entailment: the logic of relevance and necessity, Princeton University Press, Princeton, New Jersey, 1975.Google Scholar
[Avr87]Avron, A., Simple consequence relations, Information and Computation, vol. 92 (1991), pp. 105139.CrossRefGoogle Scholar
[Ben79]van Benthem, J. F. A. K., Syntactic aspects of modal incompleteness theorems, Theoria, vol. 45 (1979), pp. 6377.CrossRefGoogle Scholar
[Che80]Chellas, B. F., Modal logic, Cambridge University Press, Cambridge, 1980.CrossRefGoogle Scholar
[Chu56]Church, A., Introduction to mathematical logic. Vol. I, Princeton University Press, Princeton, New Jersey, 1956.Google Scholar
[Coo71]Cook, S. A., The complexity of theorem proving procedures, Proceedings of the third ACM symposium on theory of computing, ACM, New York, 1971, pp. 151158.Google Scholar
[CR79]Cook, S. A. and Reckhow, R. A., The relative efficiency of propositional proof systems, this Journal, vol. 44 (1979), pp. 3650.Google Scholar
[Dun86]Dunn, J. M., Relevance logic and entailment. Handbook of philosophical logic, Vol. 111 (Gabbay, D. and Guenthner, F., editors), Reidel, Dordrecht, 1986, pp. 117224.CrossRefGoogle Scholar
[Ehr61]Ehrenfeucht, A., An application of games to the completeness problem for formalized theories, Fundamenta Mathematicae, vol. 49 (1961), pp. 129141.CrossRefGoogle Scholar
[End72]Enderton, H. B., A mathematical introduction to logic, Academic Press, New York, 1972.Google Scholar
[Fag90]Fagin, R., Finite-model theory—a personal perspective, ICDT '90 (Proceedings of the 1990 international conference on database theory; Abiteboul, S. and Kanellakis, P., editors), Lecture Notes in Computer Science, vol. 470, Springer-Verlag, Berlin, 1990, pp. 324. Theoretical Computer Science (to appear).Google Scholar
[FHV90]Fagin, R., Halpern, J. Y., and Vardi, M. Y., A nonstandard approach to the logical omniscience problem, Theoretical aspects of reasoning about knowledge (proceedings of the third conference, Pacific Grove, California, 1990; Parikh, R., editor), Morgan Kaufmann, San Mateo, California, 1990, pp. 4155.Google Scholar
[FL79]Fischer, M. J. and Ladner, R. E., Propositional dynamic logic of regular programs, Journal of Computer and System Sciences, vol. 18 (1979), pp. 194211.CrossRefGoogle Scholar
[Fra54]Fraïssé, R., Sur quelques classifications des systèmes de relations, Publications Scientifiques de l'Université d'Alger, vol. 1 (1954), pp. 35182.Google Scholar
[Fre79]Frege, G., Begriffsschrift, eine der arithmetischen nachgebildete Formelsprache des reinen Denkens, Halle, 1879; English translation, From Frege to Gödel; a source book in mathematical logic (van Heijenoort, J., editor), Harvard University Press, Cambridge, Massachusetts, 1967, pp. 1–82.Google Scholar
[Fri75]Friedman, H., One hundred and two problems in mathematical logic, this Journal, vol. 40 (1975), pp. 113129.Google Scholar
[Gab76]Gabbay, D., Investigations in modal and tense logics, Reidel, Dordrecht, 1976.Google Scholar
[Gab81]Gabbay, D., Semantical investigations in Heyting's intuitionistic logic, Reidel, Dordrecht, 1981.CrossRefGoogle Scholar
[GJ79]Garey, M. and Johnson, D. S., Computers and intractibility: a guide to the theory of NP-completeness, Freeman, San Francisco, California, 1979.Google Scholar
[GP89]Goranko, V. and Passy, S., Using the universal modality: profits and questions, unpublished manuscript, 1989.Google Scholar
[Hac79]Hacking, I., What is logic? Journal of Philosophy, vol. 76 (1979), pp. 285319.CrossRefGoogle Scholar
[Hal87]Halpern, J. Y., Using reasoning about knowledge to analyze distributed systems, Annual Review of Computer Science, vol. 2 (1987), pp. 3768.CrossRefGoogle Scholar
[HC78]Hughes, G. E. and Cresswell, M. J., An introduction to modal logic, Methuen, London, 1978.Google Scholar
[HC84]Hughes, G. E. and Cresswell, M. J., A companion to modal logic, Methuen, London, 1984.Google Scholar
[HU79]Hopcroft, J. E. and Ullman, J. D., Introduction to automata theory, languages and computation, Addison-Wesley, Reading, Massachusetts, 1979.Google Scholar
[Hum86]Humberstone, I. L., A more discriminating approach to modal logic, this Journal, vol. 51 (1986), pp. 503504 (abstract only). There is also an expanded, but unpublished, manuscript.Google Scholar
[Kap87]Kapron, B., Modal sequents and definability, this Journal, vol. 52 (1987), pp. 756762.Google Scholar
[Lad77]Ladner, R. E., The computational complexity of provability in systems of modal propositional logic, SIAM Journal on Computing, vol. 6 (1977), pp. 467480.CrossRefGoogle Scholar
[LL59]Lewis, C. I. and Langford, C. H., Symbolic logic, 2nd ed., Dover, New York, 1959.Google Scholar
[Min76]Mints, G., The derivability of admissible rules, Journal of Soviet Mathematics, vol. 6 (1976), pp. 417421.CrossRefGoogle Scholar
[MSM81]Meyer, A. R., Streett, R. S., and Mirkowska, G., The deducibility problem in propositional dynamic logic, Automata, languages and programming, proceedings, Akko, 1979 (Engeler, E., editor), Lecture Notes in Computer Science, vol. 125, Springer-Verlag, Berlin, 1981, pp. 238248.Google Scholar
[Pra79]Pratt, V. R., Models of program logics, Proceedings of the 20th IEEE symposium on foundations of computer science, IEEE Computer Society Press, Washington, D. C., 1979, pp. 115122.Google Scholar
[PY82]Papadimitriou, C. H. and Yannakakis, M., The complexity of facets (and some facets of complexity), Journal of Computer and System Sciences, vol. 28 (1982), pp. 244259.CrossRefGoogle Scholar
[Qui50]Quine, W. V. O., Methods of logic, Holt, New York, 1950.Google Scholar
[Rog67]Rogers, H. Jr., Theory of recursive functions and effective computability, McGraw-Hill, New York, 1967.Google Scholar
[RR72]Routley, R. and Routley, V., Semantics of first degree entailment, Noûs, vol. 6 (1972), pp. 335359.CrossRefGoogle Scholar
[Ryb87a]Rybakov, V. V., Bases of admissible rules of the modal system Grz and of intuitionistic logic, Mathematics of the USSR Sbornik, vol. 56 (1987), pp. 311331.CrossRefGoogle Scholar
[Ryb87b]Rybakov, V. V., Decidability of admissibility in the modal system Grz and in intuitionistic logic, Mathematics of the USSR Izvestiya, vol. 28 (1987), pp. 589608.CrossRefGoogle Scholar
[Ryb89]Rybakov, V. V., Problems of admissibility and substitution, logical equations and restricted theories of free algebras, Logic, methodology and philosophy of science. VIII (Fenstad, J. E.et al., editors), North-Holland, Amsterdam, 1989, pp. 121139.Google Scholar
[Ryb90a]Rybakov, V. V., Logical equations and admissible rules of inference with parameters in modal provability logics, Studia Logica, vol. 49 (1990), pp. 215239.CrossRefGoogle Scholar
[Ryb90b]Rybakov, V. V., Problems of substitution and admissibility in the modal system Grz and in intuitionistic propositional calculus, Annals of Pure and Applied Logic, vol. 50 (1990), pp. 71106.CrossRefGoogle Scholar
[Sav70]Savitch, W. J., Relationships between nondeterministic and deterministic tape complexities, Journal of Computer and System Sciences, vol. 4 (1970), pp. 177192.CrossRefGoogle Scholar
[St087]Stockmeyer, L. J., Classifying the computational complexity of problems, this Journal, vol. 52 (1987), pp. 143.Google Scholar
[Th075a]Thomason, S., The logic consequence relation of propositional tense logic, Zeitschrift für Mathematische Logik und Grundlagen der Mathematik, vol. 21 (1975), pp. 2940.CrossRefGoogle Scholar
[Tho75b]Thomason, S., Reduction of second-order logic to modal logic, Zeitschrift für Mathematische Logik und Grundlagen der Mathematik, vol. 21 (1975), pp. 107114.CrossRefGoogle Scholar
[Tsi77]Tsitkin, A. I., On admissible rules of intuitionistic propositional calculus, Matematicheskit Sbornik, vol. 102 (1977), pp. 314323; English translation, Mathematics of the USSR—Sbornik, vol. 31 (1977), pp. 279–288.Google Scholar
[vN27]von Neumann, J., Zur Hilbertschen beweistheorie, Mathematische Zeitschrift, vol. 26 (1927), pp. 146.CrossRefGoogle Scholar