Theorem proving as constraint solving with coherent logic
type: Item
instance of: scholarly article
title: Theorem proving as constraint solving with coherent logic
author: Predrag Janičić
author: Julien Narboux
published in: Journal of Automated Reasoning
publication date: 2022-12-12T00:00:00Z
Mathematics Subject Classification ID: 68V15
zbMATH DE Number: 7632090
zbMATH Keywords: automated theorem proving
zbMATH Keywords: interactive theorem proving
zbMATH Keywords: constraint solving
zbMATH Keywords: coherent logic
zbMATH Keywords: SAT/SMT solving
describes a project that uses: URSA
describes a project that uses: AVATAR
describes a project that uses: VAMPIRE
describes a project that uses: HOLyHammer
describes a project that uses: Sledgehammer
describes a project that uses: SATzilla
describes a project that uses: Zenon
describes a project that uses: Coq
describes a project that uses: ArgoCLP
describes a project that uses: z3
describes a project that uses: Isabelle
describes a project that uses: iProver
describes a project that uses: clasp
describes a project that uses: TPTP
describes a project that uses: leanCoP
describes a project that uses: SPASS
describes a project that uses: Isabelle/HOL
MaRDI profile type: Publication
full work available at URL: s10817-022-09629-z
OpenAlex ID: W4281252527
Wikidata QID: Q113901232
cites work: Finding good proofs for description logic entailments using recursive quality measures
cites work: Automating Resolution is NP-Hard
cites work: A FORMAL SYSTEM FOR EUCLID’SELEMENTS
cites work: Proof-checking Euclid
cites work: Q4665735
cites work: Automating Coherent Logic
cites work: On the mechanization of the proof of Hessenberg's theorem in coherent logic
cites work: Q5503674
cites work: Hammering towards QED
cites work: Automatic Proof and Disproof in Isabelle/HOL
cites work: Semi-intelligible Isar proofs from machine-generated proofs
cites work: Extending Sledgehammer with SMT solvers
cites work: More SPASS with Isabelle
cites work: Encoding first order proofs in SMT
cites work: Zenon: An Extensible Automated Theorem Prover Producing Checkable Proofs
cites work: Parallel postulates and continuity axioms: a mechanized study in intuitionistic logic using Coq
cites work: Fast LCF-Style Proof Reconstruction for Z3
cites work: Reducing higher-order theorem proving to a sequence of SAT problems
cites work: The vectorization of ITPACK 2C
cites work: Inductive logic programming at 30
cites work: Practical Proof Search for Coq by Type Inhabitation
cites work: Hammer for Coq: automation for dependent type theory
cites work: Encoding First Order Proofs in SAT
cites work: Geometrisation of first-order logic
cites work: Permutability of proofs in intuitionistic sequent calculi
cites work: A fully automatic theorem prover with human-style output
cites work: Conflict-Driven Answer Set Enumeration
cites work: URSA: A System for Uniform Reduction to SAT
cites work: Q4874803
cites work: The area method. A recapitulation
cites work: A review and prospect of readable machine proofs for geometry theorems
cites work: HOL(y)Hammer: online ATP service for HOL Light
cites work: Proof simplification and automated theorem proving
cites work: Q5813181
cites work: iProver – An Instantiation-Based Theorem Prover for First-Order Logic (System Description)
cites work: On preprocessing techniques and their impact on propositional model counting
cites work: Sheaves in geometry and logic: a first introduction to topos theory
cites work: Q2479551
cites work: Short Proofs Are Hard to Find
cites work: Isabelle/HOL. A proof assistant for higher-order logic
cites work: Subsumption Algorithms for Three-Valued Geometric Resolution
cites work: Geometric Resolution: A Proof Procedure Based on Finite Model Search
cites work: IeanCOP: lean connection-based theorem proving
cites work: Isabelle. A generic theorem prover
cites work: Local Search for Unsatisfiability

Theorem proving as constraint solving with coherent logic (cites work)
cites work: Reliable reconstruction of fine-grained proofs in a proof assistant

Theorem proving as constraint solving with coherent logic (cites work)
cites work: Interlude: About the First Theorem

Theorem proving as constraint solving with coherent logic (cites work)
cites work: A Vernacular for Coherent Logic

Theorem proving as constraint solving with coherent logic (cites work)
cites work: A Coherent Logic Based Geometry Theorem Prover Capable of Producing Formal and Readable Proofs

Theorem proving as constraint solving with coherent logic (cites work)
cites work: The TPTP World – Infrastructure for Automated Reasoning

Theorem proving as constraint solving with coherent logic (cites work)
cites work: Hilbert's twenty-fourth problem

Theorem proving as constraint solving with coherent logic (cites work)
cites work: ATP and presentation service for Mizar formalizations

Theorem proving as constraint solving with coherent logic (cites work)
cites work: Finding shortest proofs: An application of linked inference rules

Theorem proving as constraint solving with coherent logic (cites work)
cites work: AVATAR: The Architecture for First-Order Theorem Provers

Theorem proving as constraint solving with coherent logic (cites work)
cites work: Types for Proofs and Programs

Theorem proving as constraint solving with coherent logic (cites work)
cites work: Automating the search for elegant proofs

Theorem proving as constraint solving with coherent logic (cites work)
cites work: Q3624141

Theorem proving as constraint solving with coherent logic (DOI)
DOI: 10.1007/S10817-022-09629-Z