In 1960 M. Davis and H. Putnam introduced some logical verification procedure for propositional languages - called later Putnam-Davis procedure. It found a broad application in AI as a basis of the planning paradigm based on satisfiability of formulas. Unfortunately, this procedure refers to satisfiability in a classical two-valued logic. This paper is aimed at proposing some multi-valued extension of this procedure that may be sensitive to temporal and preferential aspects of reasoning. This method is evaluated in more practical contexts.
展开▼
