计算机应用研究
計算機應用研究
계산궤응용연구
APPLICATION RESEARCH OF COMPUTERS
2011年
12期
4429-4432
,共4页
命题逻辑%启发式方法%试探法%自然推理法%可读证明
命題邏輯%啟髮式方法%試探法%自然推理法%可讀證明
명제라집%계발식방법%시탐법%자연추리법%가독증명
探讨了自动生成命题逻辑系统R的可读证明.采用试探法和自然推理法分别从前推和后推模拟人类思维求证,试探法根据推理规则将待证公式反向分解,自然推理法从假设出发根据推理规则生成新的公式.两种方法都实现了相干命题逻辑系统R的可读证明,并结合实现了混合证明.试探法和自然推理法是生成可读证明的有效方法,前推和后推两种思维方法也适用于其他逻辑系统的自动证明.
探討瞭自動生成命題邏輯繫統R的可讀證明.採用試探法和自然推理法分彆從前推和後推模擬人類思維求證,試探法根據推理規則將待證公式反嚮分解,自然推理法從假設齣髮根據推理規則生成新的公式.兩種方法都實現瞭相榦命題邏輯繫統R的可讀證明,併結閤實現瞭混閤證明.試探法和自然推理法是生成可讀證明的有效方法,前推和後推兩種思維方法也適用于其他邏輯繫統的自動證明.
탐토료자동생성명제라집계통R적가독증명.채용시탐법화자연추리법분별종전추화후추모의인류사유구증,시탐법근거추리규칙장대증공식반향분해,자연추리법종가설출발근거추리규칙생성신적공식.량충방법도실현료상간명제라집계통R적가독증명,병결합실현료혼합증명.시탐법화자연추리법시생성가독증명적유효방법,전추화후추량충사유방법야괄용우기타라집계통적자동증명.
