scientific article; zbMATH DE number 1765682
From MaRDI portal
Publication:4539622
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
Title of this publication is not available (Why is that?)
Recommendations
Cited In (15)
- Abstraction and resolution modulo AC: How to verify Diffie--Hellman-like protocols automatically
- Lash 1.0 (system description)
- Saturation-based Boolean conjunctive query answering and rewriting for the guarded quantification fragments
- Automatic construction and verification of isotopy invariants
- Alternating two-way AC-tree automata
- Using tableau to decide description logics with full role negation and identity
- Computer supported mathematics with \(\Omega\)MEGA
- Superposition-based equality handling for analytic tableaux
- Resolution with order and selection for hybrid logics
- \( \alpha \)-paramodulation method for a lattice-valued logic \(L_nF(X)\) with equality
- A strict constrained superposition calculus for graphs
- Title not available (Why is that?)
- Limited resource strategy in resolution theorem proving
- Translating higher-order clauses to first-order clauses
- Automation for interactive proof: first prototype
Uses Software
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)
