Carine theorem prover
Encyclopedia
CARINE is a first-order
classical logic
automated theorem prover.
CARINE (Computer Aided Reasoning engINE) is a resolution based theorem prover initially built for the study of the enhancement effects of the strategies delayed clause-construction
(DCC) and attribute sequences (ATS) in a depth-first search based algorithm [Haroun 2005]. CARINE's main search algorithm is semi-linear resolution
(SLR) which is based on an iteratively-deepening depth-first search (also known as depth-first iterative-deepening (DFID) [Korf 1985]) and used in theorem provers like THEO [Newborn 2001]. SLR employs DCC to achieve a high inference rate, and ATS to reduce the search space.
DCC is useful when too many intermediate clauses (especially first-order clauses) are being constructed and discarded in a short period of time because the operations performed to construct such short lived clauses are avoided. DCC may not be very effective on theorems with only propositional clauses.
An example of a clause as a disjunction of literals is:
~wealthy(Y) \/ ~smart(Y) \/ ~beautiful(Y) \/ loves(X, Y)
where the symbols \/ and ~ are, respectively, OR and NOT.
The above example states that if Y is wealthy AND smart AND beautiful then X loves Y. It does not say who X and Y are though. Note that the above representation comes from the logical statement:
For all Y, X belonging to the domain of human beings:
wealthy(Y) /\ smart(Y) /\ beautiful(Y) => loves(X,Y)
By using some transformation rules of formal logic we produce the disjunction of literals of the example given above.
X and Y are variables. ~wealthy, ~smart, ~beautiful, loves are literals.
Suppose we substitute the variable X for the constant John and the variable Y for the constant Jane then the above clause will become:
~wealthy(Jane) \/ ~smart(Jane) \/ ~beautiful(Jane) \/ loves(John, Jane)
A clause attribute is a characteristic of a clause. Some examples of clause attributes are:
- the number of literals in a clause (i.e., clause length)
- the number of term symbols in a clause
- the number of constants in a clause
- the number of variables in a clause
- the number of functions in a clause
- the number of negative literals in a clause
- the number of positive literals in a clause
- the number of distinct variables in a clause
- the maximum depth of any term in all the literals in a clause
Example:
the clause
C = ~P(x) \/ Q(a,b,f(x))
has a length of 2 because it contains 2 literals
1 negative literal which is ~P(x)
1 positive literal which is Q(a,b,f(x))
2 constants which are a and b
2 variables (x occurs twice)
1 distinct variable which is x
1 function which is f
maximum term depth of 2
5 term symbols which are x,a,b,f,x
An attribute sequence is a sequence of k n-tuples of clause attributes that represent a projection of a set of derivations of length k. k and n are strictly positive integers. The set of derivations form the domain and the attribute sequences form the codomain of the mapping between derivations and attribute sequences.
Example:
<(2,2),(2,1),(1,1)> is an attribute sequence where k=3 and n=2.
It corresponds to some derivation, say, <(B1,B2),(R1,B3),(R2,B4)> where B1, B2, R1, B3, R2, and B4 are clauses.
The attribute here is assumed to be the length of a clause.
The first pair (2,2) corresponds to the pair (B1,B2) from the derivation. It indicates that the length of B1 is 2 and the length of B2 is also 2.
The second pair (2,1) corresponds to the pair (R1,B3) and it indicates that the length of R1 is 2 and the length of B3 is 1.
The last pair (1,1) corresponds to the pair (R2,B4) and it indicates that the length of R2 is 1 and the length of B4 is 1.
Note: An n-tuple of clause attributes is similar (but not the same) to the feature vector named by Stephan Schulz, PhD (see E equational theorem prover
).
First-order logic
First-order logic is a formal logical system used in mathematics, philosophy, linguistics, and computer science. It goes by many names, including: first-order predicate calculus, the lower predicate calculus, quantification theory, and predicate logic...
classical logic
Classical logic
Classical logic identifies a class of formal logics that have been most intensively studied and most widely used. The class is sometimes called standard logic as well...
automated theorem prover.
CARINE (Computer Aided Reasoning engINE) is a resolution based theorem prover initially built for the study of the enhancement effects of the strategies delayed clause-construction
Delayed clause construction
Delayed Clause Construction is a method of improving the efficiency of automated theorem provers.Used in the CARINE theorem prover, DCC is a stalling strategy that enhances a theorem prover's performance by reducing the work to construct clauses to a minimum...
(DCC) and attribute sequences (ATS) in a depth-first search based algorithm [Haroun 2005]. CARINE's main search algorithm is semi-linear resolution
Semi-linear resolution
Semi-Linear Resolution is a search strategy that is based on an iteratively-deepening depth-first search...
(SLR) which is based on an iteratively-deepening depth-first search (also known as depth-first iterative-deepening (DFID) [Korf 1985]) and used in theorem provers like THEO [Newborn 2001]. SLR employs DCC to achieve a high inference rate, and ATS to reduce the search space.
Delayed Clause Construction (DCC)
Delayed Clause Construction is a stalling strategy that enhances a theorem prover's performance by reducing the work to construct clauses to a minimum. Instead of constructing every conclusion (clause) of an applied inference rule, the information to construct such clause is temporarily stored until the theorem prover decides to either discard the clause or construct it. If the theorem prover decides to keep the clause, it will be constructed and stored in memory, otherwise the information to construct the clause is erased. Storing the information from which an inferred clause can be constructed require almost no additional CPU operations. However, constructing a clause may consume a lot of time. Some theorem provers spend 30%-40% of their total execution time constructing and deleting clauses. With DCC this wasted time can be salvaged.DCC is useful when too many intermediate clauses (especially first-order clauses) are being constructed and discarded in a short period of time because the operations performed to construct such short lived clauses are avoided. DCC may not be very effective on theorems with only propositional clauses.
Attribute Sequences (ATS)
(An informal definition of) a clause in theorem proving is a statement that can result in a true or false answer depending on the evaluation of its literals. A clause is represented as a disjunction (i.e., OR), conjunction (i.e., AND), set, or multi-set (similar to a set but can contain identical elements) of literals.An example of a clause as a disjunction of literals is:
~wealthy(Y) \/ ~smart(Y) \/ ~beautiful(Y) \/ loves(X, Y)
where the symbols \/ and ~ are, respectively, OR and NOT.
The above example states that if Y is wealthy AND smart AND beautiful then X loves Y. It does not say who X and Y are though. Note that the above representation comes from the logical statement:
For all Y, X belonging to the domain of human beings:
wealthy(Y) /\ smart(Y) /\ beautiful(Y) => loves(X,Y)
By using some transformation rules of formal logic we produce the disjunction of literals of the example given above.
X and Y are variables. ~wealthy, ~smart, ~beautiful, loves are literals.
Suppose we substitute the variable X for the constant John and the variable Y for the constant Jane then the above clause will become:
~wealthy(Jane) \/ ~smart(Jane) \/ ~beautiful(Jane) \/ loves(John, Jane)
A clause attribute is a characteristic of a clause. Some examples of clause attributes are:
- the number of literals in a clause (i.e., clause length)
- the number of term symbols in a clause
- the number of constants in a clause
- the number of variables in a clause
- the number of functions in a clause
- the number of negative literals in a clause
- the number of positive literals in a clause
- the number of distinct variables in a clause
- the maximum depth of any term in all the literals in a clause
Example:
the clause
C = ~P(x) \/ Q(a,b,f(x))
has a length of 2 because it contains 2 literals
1 negative literal which is ~P(x)
1 positive literal which is Q(a,b,f(x))
2 constants which are a and b
2 variables (x occurs twice)
1 distinct variable which is x
1 function which is f
maximum term depth of 2
5 term symbols which are x,a,b,f,x
An attribute sequence is a sequence of k n-tuples of clause attributes that represent a projection of a set of derivations of length k. k and n are strictly positive integers. The set of derivations form the domain and the attribute sequences form the codomain of the mapping between derivations and attribute sequences.
Example:
<(2,2),(2,1),(1,1)> is an attribute sequence where k=3 and n=2.
It corresponds to some derivation, say, <(B1,B2),(R1,B3),(R2,B4)> where B1, B2, R1, B3, R2, and B4 are clauses.
The attribute here is assumed to be the length of a clause.
The first pair (2,2) corresponds to the pair (B1,B2) from the derivation. It indicates that the length of B1 is 2 and the length of B2 is also 2.
The second pair (2,1) corresponds to the pair (R1,B3) and it indicates that the length of R1 is 2 and the length of B3 is 1.
The last pair (1,1) corresponds to the pair (R2,B4) and it indicates that the length of R2 is 1 and the length of B4 is 1.
Note: An n-tuple of clause attributes is similar (but not the same) to the feature vector named by Stephan Schulz, PhD (see E equational theorem prover
E equational theorem prover
E is a modern, high performance theorem prover for full first-order logic with equality. It is based on the equational superposition calculus and uses a purely equational paradigm. It has been integrated into other theorem provers and it has been among the best-placed systems in several theorem...
).