Paper Info
Title
Non-cyclic Sorts for First-Order Satisfiability.
Abstract
In this paper we investigate the finite satisfiability problem for first-order logic. We show that the finite satisfiability problem can be represented as a sequence of satisfiability problems in a fragment of many-sorted logic, which we call the non-cyclic fragment. The non-cyclic fragment can be seen as a generalisation of the effectively propositional fragment (EPR) in the many-sorted setting. We show that the non-cyclic fragment is decidable by instantiation-based methods and present a linear time algorithm for checking whether a given clause set is in this fragment. One of the distinctive features of our finite satisfiability translation is that it avoids unnecessary flattening of terms, which can be crucial for efficiency. We implemented our finite model finding translation in iProver and evaluated it over the TPTP library. Using our translation it was possible solve a large class of problems which could not be solved by other systems.
Year
Venue
Field
2013
Lecture Notes in Computer Science
Discrete mathematics,Finite satisfiability,Flattening,Computer science,Generalization,First order,Satisfiability,Model finding,Decidability,Time complexity
DocType
Volume
ISSN
Conference
8152
0302-9743
Citations 
PageRank 
References 
4
0.41
29
Authors
1
Name
Order
Citations
PageRank
Konstantin Korovin128820.64