scientific article; zbMATH DE number 1765674

zbMath0988.68595MaRDI QIDQ4539610

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

Publication date: 10 July 2002

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

Title: zbMATH Open Web Interface contents unavailable due to conflicting licenses.

Mathematics Subject Classification ID

Related Items

A set automaton to locate all pattern matches in a term ⋮ The higher-order prover \textsc{Leo}-II ⋮ Things to know when implementing KBO ⋮ Limited resource strategy in resolution theorem proving ⋮ LEO-II - A Cooperative Automatic Theorem Prover for Classical Higher-Order Logic (System Description) ⋮ Citius altius fortius ⋮ Efficient instance retrieval with standard and relational path indexing ⋮ An efficient subsumption test pipeline for BS(LRA) clauses

Uses Software

• OTTER
• VAMPIRE
• TPTP