Extensions to logic programming motivated by the construction of a generic theorem prover

2006 ◽  
pp. 223-244 ◽  
Author(s):  
Elsa L. Gunter
Keyword(s):  
Logic Programming ◽  
Theorem Prover

ON A THEOREM PROVER FOR VARIATIONAL LOGIC PROGRAMS WITH FUNCTORS SETU AND SETS

2000 ◽  
Vol 08 (01) ◽  
pp. 73-92 ◽  
Author(s):  
HIROSHI SAKAI ◽  
AKIMICHI OKUMA
Keyword(s):  
Logic Programming ◽  
Soft Computing ◽  
Logic Program ◽  
Theorem Prover ◽  
Logic Programs

We are now touching a problem how we add soft computing aspects to logic programming and we have been discussing null attribute values on logic programs. Here, we introduce two functors setu and sets into logic programs for describing indefinite attribute values explicitly. Every logic program with setu or sets has variability and tolerance in itself, namely this program expresses a set of possible definite logic programs. We call this program a variational logic program. In this paper, we show the variational logic programs and a theorem prover for them.

Evaluation Opportunities in Mechanized Theories

10.29007/7kx8 ◽  
2018 ◽  
Author(s):  
Joe Hurd
Keyword(s):  
Mathematical Theory ◽  
Theorem Prover ◽  
Mechanized Mathematics ◽  
Reasoning Tasks

This invited talk will look at logic solvers through the application lens of constructing and processing a theory library of mechanized mathematics. In fact, constructing and processing theories are two distinct applications, and each will be considered in turn. Construction is carried out by formalizing a mathematical theory using an interactive theorem prover, and logic solvers can remove much of the drudgery by automating common reasoning tasks. At the theory library level, logic solvers can provide assistance with theory engineering tasks such as compressing theories, managing dependencies, and constructing new theories from reusable theory components.

Sign in / Sign up

Export Citation Format

Share Document