From arithmetic expressions to propositional formulae

• Autorzy: Stępień L. , Stępień M. R.

Identyfikatory

DOI

10.16926/m.2016.21.12

• Języki publikacji: EN

Abstrakty

EN

In papers [3], [4], [5] Authors presented a new method of solving some kinds of computational tasks in the area of linear algebra by applying SAT-solver as the highly optimized algorithms for solving the problem of propositional satisfiability. On input SAT-solver (cf. [1], [2]) takes a propositional formula in the clause form. In this paper we show in detail how any arithmetical expression can be translated into propositional formula in the CNF form skipping out its traditional form. For this, we define the notion of consistency of arithmetic and boolean valuations.

Słowa kluczowe

EN

linear algebra; declarative programming; SAT solver

PL

algebra liniowa; programowanie deklaratywne; SAT solver

• 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: 2016
• Tom: Vol. 21
• Strony: 135--143
• Opis fizyczny: Bibliogr. 6 poz.

Twórcy

autor

Stępień L.

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

autor

Stępień M. R.

• Kielce University of Technology, Department of Mathematics and Physics, al. Tysiąclecia Państwa Polskiego 7, 25-314 Kielce, Poland

Bibliografia

• [1] M. Davis, H. Putnam, A Computing Procedure for Quantification Theory, J. of the ACM 7(1) (1960), 201-215.
• [2] M. Davis, G. Logemann, D.W. Loveland, A Machine Program for Theorem Proving, Comm. of the ACM 5(7) (1962), 394-397.
• [3] M. Srebrny, L. St¸epien, A propositional programming environment for linear algebra, Fundamenta Informaticae, 81 (2007), 325-345.
• [4] M. Srebrny, L. St¸epien, SAT as a Programming Environment for Linear Algebra, Fundamenta Informaticae, 102(1) (2010), 115-127.
• [5] L. St¸epien, Propositional calculus as a programming environment for linear algebra, PhD thesis (in polish), Inst. of Comp. Science, Polish Academy of Science, Warsaw, Poland, 2009.
• [6] L. St¸epien, M. R. St¸epien, Automatic search of automorphisms of Witt rings, Scientific Issues. Mathematics, XVI (2011), 141-146, Jan Długosz University, Częstochowa.