Elimination of negation in a logical framework

DOI10.1007/3-540-44622-2_28MaRDI QIDQ2753689zbMATH OpenFDO

Authors Alberto Momigliano

Publication date 11 November 2001

Published in Lecture Notes in Computer Science (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/3-540-44622-2_28

Mathematics Subject Classification ID

Logic in computer science (03B70) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30) Specification and verification (program logics, model checking, etc.) (68Q60)

Recommendations

• scientific article; zbMATH DE number 1215501
• Success and failure for hereditary Harrop formulae
• Minimal negation and hereditary Harrop formulae
• Elimination of negation in term algebras
• scientific article; zbMATH DE number 4185011

Cited in

(9)

• Eliminating disjunctions of leads-to properties
• Eliminating disjunctions by disjunction elimination
• Automated reasoning with restricted intensional sets
• scientific article; zbMATH DE number 5354051 (Why is no real title available?)
• αCheck: A mechanized metatheory model checker
• Benchmarks for reasoning with syntax trees containing binders and contexts of assumptions
• DYNAMIC NEGATION AND NEGATIVE INFORMATION
• More Church-Rosser proofs in \textsc{Beluga}
• Anti-patterns for rule-based languages

Describes a project that uses

Uses Software

• Coq

This page was built for publication: Elimination of negation in a logical framework

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2753689)