moratori / clover Goto Github PK

A experimental prover written in Common Lisp, based on clause resolution and Knuth-Bendix completion algorithm.

Common Lisp 99.19% Shell 0.81%

prover theorem-proving theorem-prover proof-assistant symbolic-computation common-lisp logic logic-programming refutation-tree term-rewriting

clover's People

Contributors

Stargazers

Watchers

clover's Issues

特定節集合に対する効率的な導出アルゴリズムを実装する

ホーン節集合に対するSLD導出など

空節の表示方法

□を表示するなどする

単一化子のリバース

単一化子を遡り、入力変数が最終的になにに置き換えられたか表示できるようにする

CUIの実装

CUIを実装する

反駁木の描画

導出反駁木を描画する

print-objectの実装変更

print-objectが出力した内容をそのまま、parserが読める様修正

別フォーマットをパースした時の式集合の同値性について

clover/src/parser.lisp

Lines 35 to 66 in 770ff24

 (defun parse-premise-logical-expression (string) 

 (handler-case 

 (with-lexer (lexer 'premise-expression-lexer string) 

 (with-token-reader (token-reader lexer) 

 (parse-with-lexer token-reader %premise-expression-parser))) 

 (condition (con) 

 (error (make-condition 'expr-parse-error 

 :message 

 (format nil "~A error occurred while parsing string: ~A" con string)))))) 

 (defun parse-conseq-logical-expression (string) 

 (handler-case 

 (with-lexer (lexer 'conseq-expression-lexer string) 

 (with-token-reader (token-reader lexer) 

 (parse-with-lexer token-reader %conseq-expression-parser))) 

 (condition (con) 

 (error (make-condition 'expr-parse-error 

 :message 

 (format nil "~A error occurred while parsing string: ~A" con string)))))) 

 (defun parse-mkbtt-expression (string) 

 (handler-case 

 (with-lexer (lexer 'mkbtt-toplevel-lexer string) 

 (with-token-reader (token-reader lexer) 

 (convert-to-equation-set 

 (mkbtt-form 

 (parse-with-lexer token-reader %mkbtt-form-parser))))) 

 (condition (con) 

 (error (make-condition 'expr-parse-error 

 :message 

 (format nil "~A error occurred while parsing string: ~A" con string))))))

iterative-multi-completionが遅い

readmeの整備

readmeをいい感じにかく

無応答状態の際のctrl+cを正しく扱う

unhandleな状態を正しく扱う

一度のresolutionで複数の節が消える

引数なしリテラル・関数項の表示修正

引数なしリテラルを命題変数として表示する
引数なし関数項を定数として表示する

ヒューリスティック関数の実装

節集合の探索順序を制御する関数を実装(-> IDDFS以外を実装するということ)

Knuth-Bendixの完備化アルゴリズム実装

項の解釈

下記の様な項表現は、「5」として表されるべき.
項の解釈処理をユーザーが別途で定義できるようにする

successor(successor(successor(successor(successor(ZERO)))))

等値述語に対する推論規則の追加

paramodulationの実装or完備な項書き換え系の生成

節の簡単化規則の追加

アルファベット同値類の削除
節の吸収則の実装
単一述語の除去

:set-profilerを実装

sbclの場合に限り、sb-profileを用いて、実行時の統計情報を表示する

不可解なエラーの発生

BD94_collapse.trs

f(x,C)=>x
f(C,x)=>C
B=>C
A=>C
g(x)=>x
;
;
; compilation unit aborted
; compilation unit aborted
; compilation unit aborted
;   caught 1 fatal ERROR condition
;   caught 1 fatal ERROR condition
;   caught 1 fatal ERROR condition
;
;
; compilation unit aborted
; compilation unit aborted
; compilation unit aborted
;   caught 1 fatal ERROR condition
;   caught 1 fatal ERROR condition
;   caught 1 fatal ERROR condition

TPTP_GRP460-1_theory.trs

WARNING: lparallel: Replacing lost or dead worker.
unhandled condition occurred: The task was killed.

SK90_3.24.trs

YES

(VAR x)
(RULES
 c(c(c(x))) -> c(c(x))
 b(x) -> c(x)
 a(x) -> c(x)
)
(COMMENT
 C < B < A
)
;
;
; compilation unit aborted
; compilation unit aborted
; compilation unit aborted
;   caught 1 fatal ERROR condition
;   caught 1 fatal ERROR condition
;
;   caught 1 fatal ERROR condition
;
;   caught 1 fatal ERROR condition
; compilation unit aborted
;   caught 1 fatal ERROR condition
;
; compilation unit aborted
;   caught 1 fatal ERROR condition

TPTP_SWV262-2_theory.trs

YES

(VAR z w x y)
(RULES
 c_union(c_message_oparts(x),c_message_oparts(y),TC_MESSAGE_OMSG) -> c_message_oparts(c_union(x,y,TC_MESSAGE_OMSG))
 c_union(c_insert(x,y,w),z,w) -> c_insert(x,c_union(y,z,w),w)
 c_union(C_EMPTYSET,y,x) -> y
)
(COMMENT
 C_EMPTYSET < TC_MESSAGE_OMSG < C_MESSAGE_OPARTS < C_INSERT < C_UNION
)
;
; compilation unit aborted
; compilation unit aborted
;
;   caught 1 fatal ERROR condition
; compilation unit aborted
;   caught 1 fatal ERROR condition

	(defun parse-premise-logical-expression (string)
	(handler-case
	(with-lexer (lexer 'premise-expression-lexer string)
	(with-token-reader (token-reader lexer)
	(parse-with-lexer token-reader %premise-expression-parser)))
	(condition (con)
	(error (make-condition 'expr-parse-error
	:message
	(format nil "~A error occurred while parsing string: ~A" con string))))))

	(defun parse-conseq-logical-expression (string)
	(handler-case
	(with-lexer (lexer 'conseq-expression-lexer string)
	(with-token-reader (token-reader lexer)
	(parse-with-lexer token-reader %conseq-expression-parser)))

	(condition (con)
	(error (make-condition 'expr-parse-error
	:message
	(format nil "~A error occurred while parsing string: ~A" con string))))))

	(defun parse-mkbtt-expression (string)
	(handler-case
	(with-lexer (lexer 'mkbtt-toplevel-lexer string)
	(with-token-reader (token-reader lexer)
	(convert-to-equation-set
	(mkbtt-form
	(parse-with-lexer token-reader %mkbtt-form-parser)))))
	(condition (con)
	(error (make-condition 'expr-parse-error
	:message
	(format nil "~A error occurred while parsing string: ~A" con string))))))