scientific article; zbMATH DE number 1765682

zbMATH Open0988.68607MaRDI QIDQ4539622FDOQ4539622

Authors Alexandre Riazanov, Andrei Voronkov 

Publication date 10 July 2002

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

Mathematics Subject Classification ID

Recommendations

• scientific article; zbMATH DE number 1809861
• Automated Reasoning
• Interpolation and symbol elimination in Vampire
• scientific article; zbMATH DE number 2090305
• scientific article; zbMATH DE number 1765681

Cited in

(15)

• Saturation-based Boolean conjunctive query answering and rewriting for the guarded quantification fragments
• Automatic construction and verification of isotopy invariants
• Computer supported mathematics with \(\Omega\)MEGA
• Superposition-based equality handling for analytic tableaux
• \( \alpha \)-paramodulation method for a lattice-valued logic \(L_nF(X)\) with equality
• Automation for interactive proof: first prototype
• A strict constrained superposition calculus for graphs
• Abstraction and resolution modulo AC: How to verify Diffie--Hellman-like protocols automatically
• Alternating two-way AC-tree automata
• Resolution with order and selection for hybrid logics
• Limited resource strategy in resolution theorem proving
• Lash 1.0 (system description)
• scientific article; zbMATH DE number 1809861 (Why is no real title available?)
• Translating higher-order clauses to first-order clauses
• Using tableau to decide description logics with full role negation and identity

Describes a project that uses

Uses Software

• VAMPIRE

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 Q4539622)