Powiadomienia systemowe
- Sesja wygasła!
- Sesja wygasła!
Identyfikatory
Warianty tytułu
Języki publikacji
Abstrakty
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.
Rocznik
Tom
Strony
135--143
Opis fizyczny
Bibliogr. 6 poz.
Twórcy
autor
- Jan Długosz University in Częstochowa, Institute of Mathematics and Computer Science, al. Armii Krajowej 13/15, 42-200 Częstochowa, Poland
autor
- 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.
Typ dokumentu
Bibliografia
Identyfikator YADDA
bwmeta1.element.baztech-e811a9c6-3c13-4a14-8996-8fe2a2519892