Disproving using the inverse method by iterative refinement of finite approximations

DOI10.1007/978-3-319-24312-2_11MaRDI QIDQ3455767zbMATH OpenOpenAlexFDO

Authors Taus Brock-Nannestad, Kaustuv Chaudhuri

Publication date 11 December 2015

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

Full work available at URL https://hal.inria.fr/hal-01222592/file/disproving.pdf

Mathematics Subject Classification ID

Subsystems of classical logic (including intuitionistic logic) (03B20) Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15)

Recommendations

• scientific article; zbMATH DE number 4170865
• A forward unprovability calculus for intuitionistic propositional logic
• Efficient Intuitionistic Theorem Proving with the Polarized Inverse Method
• Disproving false conjectures
• Turning decision procedures into disprovers

Cites work

• A logical characterization of forward and backward chaining in the inverse method
• Computer Science Logic
• Efficient Intuitionistic Theorem Proving with the Polarized Inverse Method
• Focusing and polarization in linear, intuitionistic, and classical logics
• Foundational proof certificates in first-order logic
• Imogen: Focusing the Polarized Inverse Method for Intuitionistic Propositional Logic
• Magically constraining the inverse method using dynamic polarity assignment
• On deciding satisfiability by theorem proving with speculative inferences
• Resolution theorem proving
• Rewrite-based Equational Theorem Proving with Selection and Simplification
• The ILTP problem library for intuitionistic logic
• The inverse method

Cited in

(3)

• A forward unprovability calculus for intuitionistic propositional logic
• scientific article; zbMATH DE number 1348458 (Why is no real title available?)
• Turning decision procedures into disprovers

Describes a project that uses

Uses Software

• ILTP
• MiniSat
• Mace4
• Imogen

This page was built for publication: Disproving using the inverse method by iterative refinement of finite approximations

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