On the evaluation of indexing techniques for theorem proving

DOI10.1007/3-540-45744-5_19MaRDI QIDQ4539610zbMATH OpenFDO

Authors Robert Nieuwenhuis, Th. Hillenbrand, Alexandre Riazanov, Andrei Voronkov

Publication date 10 July 2002

Published in Lecture Notes in Computer Science (Search for Journal in Brave)

Full work available at URL http://link.springer.de/link/service/series/0558/bibs/2083/20830257

Mathematics Subject Classification ID

Cited in

(11)

• Limited resource strategy in resolution theorem proving
• An efficient subsumption test pipeline for BS(LRA) clauses
• A set automaton to locate all pattern matches in a term
• Efficient instance retrieval with standard and relational path indexing
• The higher-order prover \textsc{Leo}-II
• LEO-II - A Cooperative Automatic Theorem Prover for Classical Higher-Order Logic (System Description)
• Citius altius fortius: lessons learned from the theorem prover Waldmeister
• Computing ground congruence classes
• SAT solving for variants of first-order subsumption
• A two-watched literal scheme for first-order logic
• Things to know when implementing KBO

Describes a project that uses

Uses Software

• TPTP
• OTTER
• VAMPIRE

This page was built for publication: On the evaluation of indexing techniques for theorem proving

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q4539610)