Tik-79.154 Logiikka tietotekniikassa:
erityiskysymyksiä II (2 ov) syksy 1997

Tenttiohje

Tentissä tulisi osata kurssilla käsitellyt menetelmät (Davis-Putnam, BDDt, paikalliset hakumenetelmät, sääntöpohjaisen päättelyn menetelmät) ja niihin liittyvät käsitteet sekä lauselogiikkaan ja logiikkaohjelmiin liittyvää mallitustekniikkaa.

Kurssimateriaali

• Fitting, M., First-Order Logic and Automated Theorem Proving, Springer-Verlag, 1990, pp. 88-93

• Crawford, J.M. and Auton, L.D., Experimental Results on the Crossover Point in Random 3-SAT, Artificial Intelligence 81 (1996) 1, 31-57.

• Bryant, R.E., Graph-based Algorithms for Boolean Function Manipulation. IEEE Transactions on Computers C-35 6 (Aug) 1986, pp. 677-691.

• Bryant, R.E., Symbolic Boolean Manipulation with Ordered Binary Decision Diagrams, ACM Computing Surveys 24 (3): 293-318 (1992). Report version

• Selman, B., Kautz, H. and Cohen B., Local Search Strategies for Satisfiability Testing, Dimacs Series in Discrete Mathematics and Theoretical Computer Science.

• Dowling, W.F. and Gallier, J.H., Linear-Time Algorithms for Testing the Satisfiability of Propositional Horn Formulae, Journal of Logic Programming 3 (1984) 267-284.

• Kautz, H. and Selman B., Planning as Satisfiability, Proceeding of the 10th European Conference on Artificial Intelligence, 1992, John Wiley and Sons, 359-363.

• Kautz, H. and Selman B., Pushing the Envelope: Planning, Propositional Logic, and Stochastic Search, Proceedings of the 13th National Conference on Artificial Intelligence, Portland, OR, 1996.