Disproving Using the Inverse Method by Iterative Refinement of Finite Approximations

DOI10.1007/978-3-319-24312-2_11zbMath1471.68303OpenAlexW2243108586MaRDI QIDQ3455767

Kaustuv Chaudhuri, Taus Brock-Nannestad

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)

Uses Software

• Mace4
• Imogen
• Unnamed Item
• Unnamed Item

Cites Work

• Unnamed Item
• Unnamed Item
• On deciding satisfiability by theorem proving with speculative inferences
• The ILTP problem library for intuitionistic logic
• A logical characterization of forward and backward chaining in the inverse method
• Focusing and polarization in linear, intuitionistic, and classical logics
• Rewrite-based Equational Theorem Proving with Selection and Simplification
• Foundational Proof Certificates in First-Order Logic
• Magically Constraining the Inverse Method Using Dynamic Polarity Assignment
• Efficient Intuitionistic Theorem Proving with the Polarized Inverse Method
• Computer Science Logic
• Imogen: Focusing the Polarized Inverse Method for Intuitionistic Propositional Logic

This page was built for publication: Disproving Using the Inverse Method by Iterative Refinement of Finite Approximations