×

Temporal theories of reasoning. (English) Zbl 0849.03018

J. Appl. Non-Class. Log. 5, No. 1, 97-119 (1995); correction No. 2, 239-261 (1995).
The authors’ aim is to describe a general way of formalizing reasoning behaviour. A particular reasoning pattern is viewed as a sequence of information states and an inference step as a transition of the current information state to the next information state. Temporal partial logic is a natural formalisation of these intuitions. The approach is considered as a first step to provide semantics of formal specification languages for reasoning systems for complex tasks and as a contribution to a better integration of dynamic aspects in logical systems.
In section 2 temporal partial logic is introduced. Flow of time, partial temporal model, interpretation of temporal formulae are defined (more detailed and precise definitions are given in the Appendix A). It is assumed in the paper that the reasoning is conservative, which means that once a fact is established, it will remain true in the future of the reasoning process. What is most interesting about a reasoning process is its set of final conclusions. The idea is formalized by the notion of limit model. The limit model \(\lim_B M\) of a branch \(B\) of (a conservative) model \(M\) is defined in a branching time model.
In section 3 homomorphisms of partial temporal models and persistency under homomorphism are defined. The model \(F\) of a temporal theory Th is called a final model of Th if for each model \(M\) of Th there is a unique homomorphism \(f : M \to F\).
In the rest of the paper temporal axiomatizations of three types of reasoning are presented.
In section 4 a temporal axiomatization of a classical proof system is given. The main idea of the axiomatization is based on a temporal interpretation of modus ponens: if in the current information state both \(A\) and \(A \to B\) have been derived then in a next information state \(B\) has been derived. However, the truth of the formulae \(A\) and \(A \to B\) in a current state implies the truth of \(B\) in the same state. To avoid this problem, a mapping is defined: for each formula \(\phi\) of the original language a new atom at\(_\phi\) is defined. A translation of the proof rules into temporal formulae is based on these ideas. A temporal translation of a proof system (a temporal theory \(\text{Th}_{PS,K}\)) has a final model.
In section 5 it is shown that default reasoning patterns (based on normal defaults) can be captured by temporal theories. The idea is that if formula \(\alpha\) has already been established in the past, and there is a possible future reasoning path where the formula \(\beta\) remains consistent, then \(\beta\) can be assumed to hold in the current time point. Let \(\text{Th}_{\Delta}\) be a temporal interpretation of a normal default theory \(\Delta\). Relations between extensions of \(\Delta\) and temporal models of \(\text{Th}_\Delta\) are studied.
Finally, in section 6, a temporal axiomatization of a meta-level architecture is presented.

MSC:

03B60 Other nonclassical logic
68T27 Logic in artificial intelligence
03B45 Modal logic (including the logic of norms)
68T30 Knowledge representation
03B80 Other applications of logic
PDFBibTeX XMLCite
Full Text: DOI

References:

[1] van Benthem, J. F.A.K. 1983. ”The logic of time: a model-theoretic investigation into the varieties of temporal ontology and temporal discourse, Reidel, Dordrecht”. · Zbl 0508.03008
[2] van Benthem, J. F.A.K. 1991. ”Logic and the flow of information”. Edited by: Prawitz, D., Skyrms, B. and Westerstahl, D. Proc. 9th Int. Congress of Logic, Methodology and Philosophy of Science, North Holland · Zbl 0758.03012
[3] Besnard, P. and Mercer, R. E. 1992. ”Non-monotonic logics: a valuations-based approach”. Edited by: du Boulay, B. and Sgurev, V. 77–84. Elsevier Science Publishers. Artificial Intelligence V: Methodology, Systems, Applications
[4] Bestougeff, H. and Ligozat, G. 1992. ”Logical tools for temporal knowledge representation, Ellis Horwood”.
[5] Blamey, S. 1986. ”Partial Logic”. Edited by: Gabbay, D. and Guenthner, F. Handbook of Philosophical Logic, Vol. III, 1–70, Reidel, Dordrecht · Zbl 0875.03023
[6] Bowen, K. A. and Kowalski, R. 1982. ”Amalgamating language and meta-language in logic programming.”. Edited by: Clark, K. and Tarnlund, S. Logic programming. Academic Press
[7] Clancey, W. J. and Bock, C. 1988. ”Representing control knowledge as abstract tasks and metarules”. Edited by: Bolc, Coombs. Expert System Applications
[8] Davis, R. 1980. ”Metarules: reasoning about control, Artificial Intelligence 15”. 179–222. · doi:10.1016/0004-3702(80)90043-0
[9] Engelfriet, J. and Treur, J. 1993. ”A temporal model theory for default logic”. Edited by: Clarke, M., Kruse, R. and Moral, S. 91–96. Springer Verlag. Proc. 2nd European Conference on Symbolic and Quantitative Approaches to Reasoning and Uncertainty, ECSQARU ’93, Extended version: Report IR-334, Vrije Universiteit Amsterdam, Department of Mathematics and Computer Science, 1993 pp. 38
[10] Engelfriet, J. and Treur, J. 1994. ”Relating linear and branching time temporal models, Report, Free University Amsterdam, Department of Mathematics and Computer Science”. · Zbl 0988.03513
[11] Engelfriet, J. and Treur, J. 1994. ”Final model semantics for normal default theories, Report, Free University Amsterdam, Department of Mathematics and Computer Science”. · Zbl 0988.03513
[12] Finger, M. and Gabbay, D. M. 1992. ”Adding a temporal dimension to a logic system, Journal of Logic, Language and Information 1”. 203–233. · Zbl 0798.03031 · doi:10.1007/BF00156915
[13] Gabbay, D. M. 1982. ”Intuitionistic basis for non-monotonic logic”. Edited by: Goos, G. and Hartmanis, J. 260–273. Springer Verlag. 6th Conference on Automated Deduction, Lecture Notes in Computer Science, vol. 138 · doi:10.1007/BFb0000064
[14] Giunchiglia, E., Traverso, P. and Giunchiglia, F. 1993. ”Multi-context Systems as a Specification framework for Complex Reasoning Systems”. Edited by: Treur, J. and Wetter, Th. Formal Specification of Complex Reasoning Systems, Ellis Horwood · Zbl 0808.68094
[15] Goldblatt, R. 1987. ”Logics of Time and Computation. CSLI Lecture Notes, vol. 7.”. Center for the Study of Language and Information · Zbl 0635.03024
[16] van Harmelen, F., Lopez de Mantaras, R., Malec, J. and Treur, J. 1993. ”Comparing formal specification languages for complex reasoning systems.”. Edited by: Treur, J. and Wetter, Th. 257–282. Formal Specification of Complex Reasoning Systems, Ellis Horwood
[17] Kripke, S. 1965. ”Semantical Analysis of Intuitionistic Logic”. Edited by: Crossley, J. N. and Dummett, M. 92–129. Formal Systems and Recursive Function Theory, North Holland
[18] Langholm, T. 1988. ”Partiality, Truth and Persistance, CSLI Lecture Notes No. 15, Stanford University, Stanford”.
[19] Maes P., Meta-level architectures and reflection (1988) · Zbl 0635.00014
[20] Reiter, R. 1980. ”A logic for default reasoning, Artificial Intelligence 13”. 81–132. · Zbl 0435.68069 · doi:10.1016/0004-3702(80)90014-4
[21] Sandewall, E. 1985. ”A functional approach to non-monotonic logics, Computational Intelligence 1”. 80–87. · doi:10.1111/j.1467-8640.1985.tb00061.x
[22] Tan, Y. H. and Treur, J. 1991. ”A bi-modular approach to nonmonotonic reasoning”. Edited by: De Glas, M. and Gabbay, D. 461–476. Proc. World Congress on Fundamentals of Artificial Intelligence, WOCFAI-91
[23] Tan, Y. H. and Treur, J. 1992. ”Constructive default logic and the control of defeasible reasoning”. Edited by: Neumann, B. 299–303. Proc. 10th European Conference on Artificial Intelligence, ECAI-92, Wiley and Sons
[24] Thijsse, E. 1992. ”Partial logic and knowledge representation, Ph.D. Thesis, Tilburg University”. · Zbl 0759.68084
[25] Treur, J. 1991. ”Declarative functionality descriptions of interactive reasoning modules”. Edited by: Boley, H. and Richter, M. M. 221–236. Springer Verlag. Processing Declarative Knowledge, Proc. of the International Workshop PDK-91, Lecture Notes in Artificial Intelligence, vol. 567
[26] Treur, J. 1994. ”Temporal semantics of meta-level architectures for dynamic control, Report, Free University Amsterdam, Department of Mathematics and Computer Science”. Shorter version in: Proc. 4th International Workshop on Meta-programming in Logic, META ’94, 1994 · Zbl 1017.68120
[27] Treur J., Formal specification of complex reasoning systems (1993) · Zbl 0827.68075
[28] Weyhrauch, R. W. 1980. ”Prolegomena to a theory of mechanized formal reasoning, Artificial Intelligence 13”. 133–170. · Zbl 0435.68070 · doi:10.1016/0004-3702(80)90015-6
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.