Cilj kolegija Uvod u formalne metode je upoznavanje studenata s osnovnim metodama simboličke logike u primjeni na razvoj programske podrške, kako klasične, tako i suvremene. Studenti će usvojiti elemente sintakse i semantike klasičnog računa sudova, te metode automatske dedukcije, zasnovane na pravilu rezolucije za račun sudova i njegovim modifikacijama (semantička rezolucija, linearna rezolucija, hiperrzolucija), odnosno na metodi Davisa-Putnama. Usvojeni formalni jezik računa sudova i njegovih podsustava (Hornova logika) i nadsustava (kvantificirani računa sudova) i za njih razvijene metode automatske dedukcije zatim će poslužiti kao sredstvo modeliranja i rješavanja cijelog niza problema (kombinatornih, problema planiranja u umjetnoj inteligenciji, problema modeliranja strateških (šah) i kombinatornih (%22četiri u nizu%22) igara), te propozicijskih informacijskih i ekspertnih sustava.