Skip to content

A presentation of a previously unexamined method for improving the efficiency of first-order logic provers

Notifications You must be signed in to change notification settings

markjm/honorsthesis

Folders and files

NameName
Last commit message
Last commit date

Latest commit

 

History

16 Commits
 
 
 
 
 
 

Repository files navigation

Honors Thesis (from Mark M @ UNC Dept of Computer Science)

Many automated theorem proving applications rely on the DPLL algorithm for deciding the satisfiability of a set of propositional logic formulae. For first-order logic formulae, ground clauses within the Herbrand universe may be exhaustively enumerated below an incrementing size-bound and fed as input to DPLL. From even a cursory investigation of these enumerated clauses, it is evident that many of them have multiple repeated terms. Here, we explore a potential method for exploiting the size-bound by “cheating in” larger clauses with many repeating terms that may be relevant to the proof.

The full notebook is viewable on github. For an in-depth discussion, I've included a copy of the final paper.

If anyone is interested in exploring or continuing this work: Try setting Repeats length to 1 :)

About

A presentation of a previously unexamined method for improving the efficiency of first-order logic provers

Resources

Stars

Watchers

Forks

Releases

No releases published

Packages

No packages published