scientific article; zbMATH DE number 1765682
From MaRDI portal
Publication:4539622
zbMath0988.68607MaRDI QIDQ4539622
Andrei Voronkov, Alexandre Riazanov
Publication date: 10 July 2002
Full work available at URL: http://link.springer.de/link/service/series/0558/bibs/2083/20830376
Title: zbMATH Open Web Interface contents unavailable due to conflicting licenses.
Related Items
Alternating two-way AC-tree automata, \( \alpha \)-paramodulation method for a lattice-valued logic \(L_nF(X)\) with equality, Computer supported mathematics with \(\Omega\)MEGA, Superposition-based equality handling for analytic tableaux, A strict constrained superposition calculus for graphs, Saturation-based Boolean conjunctive query answering and rewriting for the guarded quantification fragments, Limited resource strategy in resolution theorem proving, Resolution with order and selection for hybrid logics, Automation for interactive proof: first prototype, Automatic construction and verification of isotopy invariants, Translating higher-order clauses to first-order clauses, Using tableau to decide description logics with full role negation and identity, Abstraction and resolution modulo AC: How to verify Diffie--Hellman-like protocols automatically
Uses Software
