Abstract: 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.
B I B L I O G R A F I A[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ępień, A propositional programming environment for linear algebra,
Fundamenta Informaticae, 81 (2007), 325-345.
[4] M. Srebrny, L. Stępień, SAT as a Programming Environment for Linear Algebra,
Fundamenta Informaticae, 102(1) (2010), 115-127.
[5] L. Stępień, 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ępień, M. R. Stępień, Automatic search of automorphisms of Witt rings,
Scientific Issues. Mathematics, XVI (2011), 141-146, Jan Długosz University,
Częstochowa. 
DOI Spis treści