scientific article; zbMATH DE number 1341621

zbMath0937.03013MaRDI QIDQ4263170

Christoph Benzmüller

Publication date: 29 May 2000

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

zbMATH Keywords

resolutionautomated theorem provingparamodulationHenkin model

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35)

Related Items

Cut-elimination for quantified conditional logic, The higher-order prover \textsc{Leo}-II, Extensional higher-order paramodulation in Leo-III, Combining and automating classical and non-classical logics in classical higher-order logics, Superposition with lambdas, Superposition with lambdas, Superposition with first-class booleans and inprocessing clausification

Uses Software

• Leo