謂詞邏輯法

謂詞邏輯法採用謂詞合適公式和一階謂詞演算把要解決的問題變為一個有待證明的問題，然後採用消解定理和消解反演來證明一個新語句是從已知的正確語句導出的，從而證明這個新語句也是正確的。謂詞邏輯是一種形式語言，能夠把數學中的邏輯論證符號化。謂詞邏輯法常與其它表示方法混合使用，靈活方便，可以表示比較複雜的問題。