scientific article; zbMATH DE number 1444729

zbMath0945.03018MaRDI QIDQ4952309

Clare Dixon

Publication date: 9 May 2000

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

zbMATH Keywords

temporal logicOTTERtemporal resolutionresolution based theorem provertranslation into classical propositional logic

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35) Temporal logic (03B44)

Related Items (4)

Extracting unsatisfiable cores for LTL via temporal resolution ⋮ Theorem proving using clausal resolution: from past to present ⋮ Enhancing unsatisfiable cores for LTL with information on temporal relevance ⋮ Mechanising first-order temporal resolution

Uses Software

• OTTER

This page was built for publication: