Valuation graphs for propositional logic

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

Abstrakty

EN

In this paper we present the proof system, called the valuation graphs system, which is a new version of two proof procedures: Davis-Putnam and Stålmarck. The novelty is that in the rules we note which propositional variable occurring in some propositional formula does not determine the logical value of that formula. Due to Stålmarck, we define a notion of proof width, corresponding to the width of structure of valuation graph which is a number of applications of dilemma rule. The dilemma rule considers two cases, so the time of proof grows up exponentially.

Słowa kluczowe

EN

valuation graphs; propositional logic

PL

wykresy wyceny; rachunek zdań

• 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: 2010
• Tom: Vol. 15
• Strony: 139--148
• Opis fizyczny: Bibliogr. 8 poz., rys.

Twórcy

autor

Stępień L.

• Institute of Mathematics and Computer Science Jan Długosz University in Częstochowa al. Armii Krajowej 13/15, 42-200 Częstochowa, Poland

Bibliografia

• [1] M. Björk. A first order extension of Stålmarck's method. Department of Computer Science and Engineering Chalmers University of Technology and Göteborg University, Göteborg, Sweden, 2006.
• [2] A. Borälv. The industiral success of verification tools based on Stålmarck's method. Proc. 9th Int. Conf. on Computer Aided Verification, LNCS, vol. 1254, pp. 7-10, Springer, 1997.
• [3] M. Davis, H. Putnam. A computing procedure for quantification theory. Journal of the ACM, 7, 201-215, 1960
• [4] M. Davis, G. Logemann, D. Loveland. A machine program for theorem proving. Communications of the ACM, 5, 394-397, 1962.
• [5] M. Sheeran, G. Stålmarck. A tutorial on Stålmarck's proof procedure for propositional logic. Formal Methods in System Design, 16 (1), 23-58, 2000.
• [6] G. Stålmarck. A note on the computational complexity of the pure classical implication calculus. Inf. Process. Lett., 31 (6), 277-278, 1989.
• [7] G. Stålmarck. System for Determining Propositional Logic Theorems by Applying Values and Rules to Triplets that are Generated from a Formula. Swedish Patent No. 467076, 1992; U.S. Patent No.5276897, 1994; European Patent No. 0403454, 1995.
• [8] G. Stålmarck, M. Säflund. Modelling and verifying systems and software in propositional logic. Proc. SAFECOMP'90, pp.31-36, Pergamon Press, 1990.