Fast Automatic Deduction

• Autorzy: Stępień L.
• Języki publikacji: EN

Abstrakty

EN

Słowa kluczowe

EN

algorythm; propositional calculus; classical logic

PL

algorytm; rachunek zdań; logika klasyczna

• Wydawca: Wydawnictwo Uniwersytetu Humanistyczno-Przyrodniczego im. Jana Długosza w Częstochowie
• Czasopismo: Scientific Issues of Jan Długosz University in Częstochowa. Mathematics
• Rocznik: 2000/2001
• Tom: Vol. 8
• Strony: 89--99
• Opis fizyczny: Bibliogr. 14 poz.

Twórcy

autor

Stępień L.

• Pedagogical University Institute of Mathematics and Computer Science Al. Armii Krajowej 13/15 42-200 Częstochowa

Bibliografia

• [1] J. L. Bell, A. B. Slomson, Models and Ultraproducts: an introduction,North-Holland Publishing Company-Amsterdam-London, 1971.
• [2] E. Birnbaum, E. L. Lozinskii, The Good Old Davis-Putnam Procedure Helps Counting Models, Journal of Artificial Intelligence Research 10 (1999) 457-477.
• [3] A. Boralv and G. Stalmarck, Automated Verification in Railways, In Indastrial-Strength Formal Methods in Practice, eds. M. G. Hinchey and J. P. Bowen, Springer- Verlag, London, 1999.
• [4]M. Davis, G. Logemann, D. Loveland. A machine program for theoremproving. Communications of the ACM, 5(7): 394-397, July 1962.
• [5] M. Davis and H. Putnam: A computing procedure for quantification theory. Journal of the ACM, 7: 201-215, 1960. Reprinted in [Siekman and Wrightson, 1983].
• [6] M. C. Fitting: First-Order Logic and Automated Theorem Proving. Springer- Verlag. New York, 1990. Second Edition, Springer- Verlag, New York, 1996.
• [7] A. Grzegorczyk, Zarys logiki matematycznej, PWN, Warszawa, 1981.
• (8] J. Siekman and G. Wrightson (editors): Automation of Reasoning. Springer- Verlag, New York, 1983.
• [9] J. P. M. Silva and K. A. Sakallah, GRASP - A New Search AIgorithm for Satisfiability, Transactions on Computers, vol. 48, (no 5), pp. 506- 21, 1999.
• [10] J. P. M. Silva and K. A. Sakallah, Confiict Analysis in Search AIgorithms for Satisfiability, Technical Report RT-4-96, INESC, May 1996.
• [11] G. Stalmarck, A system for determining propositionallogic theorems by applying values and rules to triplets that are generated from a formula, 1989. Swedish Patent No. 467 076 (approved 1992), U. S. Patent No. 5 276 897 (approved 1994), European Patent No. O 403 454 (approved 1995)
• [12] Esprit project 22703. SYnchronous Reactive Formalisms SYRF, Project Programme, 1996. http://www.imag.fr/VERIMAG /SYNCHRONE/SYFR/
• [13] T. E. Uribe, M. E. Stickel. Ordered Binary Decision Diagrams and the Davis-Putnam Procedure. Lecture Notes in Computer Science, 845: 34-49, Springer- Verlag, September, 1994.
• [14] H. Zhang, SATO: A decision procedure for propositionallogic, Association for Automated Reasoning Newsletter, 22, 1-3, March 1993.