scientific article; zbMATH DE number 1765674

zbMATH Open0988.68595MaRDI QIDQ4539610FDOQ4539610

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

Publication date: 10 July 2002

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

Title of this publication is not available (Why is that?)

Mathematics Subject Classification ID

Cited In (8)

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

Uses Software

• OTTER
• VAMPIRE
• TPTP

This page was built for publication:

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