swMATH ID: 6622
Software Authors: He, Lifeng
Description: I-SATCHMO: An improvement of SATCHMO We introduce a method for reducing the redundant search space for SATCHMO’s model generation approach by means of intelligent backtracking. During the reasoning, we mark an asserted consequent atom as “useful” whenever it has been used as an antecedent atom for forward chaining. We show that a splitting of the consequence of a non-Horn clause is unnecessary if one of its consequent atoms is found not to be “useful” at the time it is retracted from the database on backtracking, and therefore the remaining splitting over the clause’s consequence can be immediately abandoned. In this way, much of the redundant search space can be eliminated. Our method is simple in principle, easy to implement in Prolog, independent of other refinements, and effective for model generation theorem proving.
Homepage: http://dl.acm.org/citation.cfm?id=594315
Programming Languages: Prolog
Keywords: SATCHMO; theorem prover; backtracking
Related Software: SATCHMO; SATCHMOREBID; TPTP; R-SATCHMO; IDV; SRASS; SNARK; Waldmeister; SigmaKEE; YAGO; SystemOnTPTP; Octopus; Ivy; MaLARea; E Theorem Prover; OMDoc; Twelf; Zenon; CSPLib; SMT-LIB
Referenced in: 5 Publications

Standard Articles

1 Publication describing the Software, including 1 Publication in zbMATH Year
I-SATCHMO: An improvement of SATCHMO. Zbl 0988.68167
He, Lifeng

Referenced in 1 Field

5 Computer science (68-XX)

Referencing Publications by Year