Theorem proving as constraint solving with coherent logic

DOI10.1007/S10817-022-09629-ZOpenAlexW4281252527WikidataQ113901232 ScholiaQ113901232MaRDI QIDQ2102932FDOQ2102932

Authors: Predrag Janičić, Julien Narboux 

Publication date: 12 December 2022

Published in: Journal of Automated Reasoning (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/s10817-022-09629-z

Recommendations

• CDCL-Based Abstract State Transition System for Coherent Logic
• A coherent logic based geometry theorem prover capable of producing formal and readable proofs
• On the mechanization of the proof of Hessenberg's theorem in coherent logic
• Automating Coherent Logic
• A vernacular for coherent logic

zbMATH Keywords

automated theorem provinginteractive theorem provingconstraint solvingcoherent logicSAT/SMT solving

Mathematics Subject Classification ID

Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15)

Cites Work

• The TPTP World -- infrastructure for automated reasoning
• A coherent logic based geometry theorem prover capable of producing formal and readable proofs
• Automatic proof and disproof in Isabelle/HOL
• Zenon: An Extensible Automated Theorem Prover Producing Checkable Proofs
• Hammer for Coq: automation for dependent type theory
• The vectorization of ITPACK 2C
• Title not available (Why is that?)
• Sheaves in geometry and logic: a first introduction to topos theory
• Isabelle. A generic theorem prover
• Isabelle/HOL. A proof assistant for higher-order logic
• SATzilla: portfolio-based algorithm selection for SAT
• ATP and presentation service for Mizar formalizations
• HOL(y)Hammer: online ATP service for HOL Light
• Extending Sledgehammer with SMT solvers
• Semi-intelligible Isar proofs from machine-generated proofs
• More SPASS with Isabelle
• iProver – An Instantiation-Based Theorem Prover for First-Order Logic (System Description)
• The area method. A recapitulation
• Types for Proofs and Programs
• Fast LCF-Style Proof Reconstruction for Z3
• A FORMAL SYSTEM FOR EUCLID’SELEMENTS
• Geometrisation of first-order logic
• URSA: a system for uniform reduction to SAT
• AVATAR: The Architecture for First-Order Theorem Provers
• Conflict-Driven Answer Set Enumeration
• Geometric Resolution: A Proof Procedure Based on Finite Model Search
• On the mechanization of the proof of Hessenberg's theorem in coherent logic
• Local Search for Unsatisfiability
• Title not available (Why is that?)
• A fully automatic theorem prover with human-style output
• Tools and algorithms for the construction and analysis of systems. 14th international conference, TACAS 2008, held as part of the joint European conferences on theory and practice of software, ETAPS 2008, Budapest, Hungary, March 29--April 6, 2008. Proceedings
• An introduction to Gödel's theorems
• Reducing higher-order theorem proving to a sequence of SAT problems
• Permutability of proofs in intuitionistic sequent calculi
• Automating the search for elegant proofs
• Reliable reconstruction of fine-grained proofs in a proof assistant
• Hammering towards QED
• Proof simplification and automated theorem proving
• IeanCOP: lean connection-based theorem proving
• Automating Resolution is NP-Hard
• A review and prospect of readable machine proofs for geometry theorems
• A Vernacular for Coherent Logic
• Parallel postulates and continuity axioms: a mechanized study in intuitionistic logic using Coq
• Hilbert's twenty-fourth problem
• Practical Proof Search for Coq by Type Inhabitation
• Finding good proofs for description logic entailments using recursive quality measures
• Finding shortest proofs: An application of linked inference rules
• Subsumption Algorithms for Three-Valued Geometric Resolution
• Inductive logic programming at 30
• On preprocessing techniques and their impact on propositional model counting
• Proof-checking Euclid
• Encoding first order proofs in SMT
• Encoding First Order Proofs in SAT
• Title not available (Why is that?)
• Title not available (Why is that?)
• Short Proofs Are Hard to Find
• Automating Coherent Logic

Cited In (5)

• Title not available (Why is that?)
• Title not available (Why is that?)
• Automated generation of illustrated proofs in geometry and beyond
• The rue theorem-proving system: The complete set of LIM+ challenge problems
• On the mechanization of the proof of Hessenberg's theorem in coherent logic

Uses Software

• Coq
• Isabelle
• Isabelle/HOL
• VAMPIRE
• SPASS
• TPTP
• z3
• SATzilla
• Zenon
• Sledgehammer
• clasp
• ArgoCLP
• iProver
• leanCoP
• HOLyHammer
• URSA
• AVATAR

This page was built for publication: Theorem proving as constraint solving with coherent logic

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