Defines non-system logical connectives, admissible logical variables, logical strings representing logical formulae in Polish (prefix) notation, conversions between them, and many functions operating on logical formulae and their sets, such as a function computing the truth table, functions converting logical formulae to conjunctive and disjunctive normal forms, functions computing resolvents and sequences of resolvents of a set of clauses, a function realizing as a table simple resolution algorithms suitable for the manual verification of the satisfiability of a set of clauses, and a function realizing the algorithm described in Anthony Galton`s book Logic for Information Technology (John Wiley & Sons, 1990, pp. 104-105) and finding and printing a refutation tree if the set of clauses is not satisfiable