Theorem proving as constraint solving with coherent logic
From MaRDI portal
Publication:2102932
DOI10.1007/s10817-022-09629-zOpenAlexW4281252527WikidataQ113901232 ScholiaQ113901232MaRDI QIDQ2102932
Julien Narboux, Predrag Janičić
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
Related Items (1)
Uses Software
Cites Work
- Semi-intelligible Isar proofs from machine-generated proofs
- The area method. A recapitulation
- Sheaves in geometry and logic: a first introduction to topos theory
- Automating the search for elegant proofs
- Permutability of proofs in intuitionistic sequent calculi
- Isabelle. A generic theorem prover
- IeanCOP: lean connection-based theorem proving
- Isabelle/HOL. A proof assistant for higher-order logic
- Hammer for Coq: automation for dependent type theory
- Parallel postulates and continuity axioms: a mechanized study in intuitionistic logic using Coq
- Hilbert's twenty-fourth problem
- ATP and presentation service for Mizar formalizations
- HOL(y)Hammer: online ATP service for HOL Light
- Finding good proofs for description logic entailments using recursive quality measures
- Reliable reconstruction of fine-grained proofs in a proof assistant
- Inductive logic programming at 30
- Reducing higher-order theorem proving to a sequence of SAT problems
- Extending Sledgehammer with SMT solvers
- On preprocessing techniques and their impact on propositional model counting
- A fully automatic theorem prover with human-style output
- A review and prospect of readable machine proofs for geometry theorems
- On the mechanization of the proof of Hessenberg's theorem in coherent logic
- 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
- Proof-checking Euclid
- GEOMETRISATION OF FIRST-ORDER LOGIC
- Subsumption Algorithms for Three-Valued Geometric Resolution
- Encoding First Order Proofs in SMT
- More SPASS with Isabelle
- AVATAR: The Architecture for First-Order Theorem Provers
- The TPTP World – Infrastructure for Automated Reasoning
- A Coherent Logic Based Geometry Theorem Prover Capable of Producing Formal and Readable Proofs
- URSA: A System for Uniform Reduction to SAT
- Automatic Proof and Disproof in Isabelle/HOL
- The vectorization of ITPACK 2C
- Zenon: An Extensible Automated Theorem Prover Producing Checkable Proofs
- iProver – An Instantiation-Based Theorem Prover for First-Order Logic (System Description)
- Encoding First Order Proofs in SAT
- Geometric Resolution: A Proof Procedure Based on Finite Model Search
- Interlude: About the First Theorem
- Practical Proof Search for Coq by Type Inhabitation
- Short Proofs Are Hard to Find
- Automating Resolution is NP-Hard
- Hammering towards QED
- Proof simplification and automated theorem proving
- Automating Coherent Logic
- Conflict-Driven Answer Set Enumeration
- A Vernacular for Coherent Logic
- Types for Proofs and Programs
- Fast LCF-Style Proof Reconstruction for Z3
- Local Search for Unsatisfiability
- A FORMAL SYSTEM FOR EUCLID’SELEMENTS
- Finding shortest proofs: An application of linked inference rules
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
This page was built for publication: Theorem proving as constraint solving with coherent logic
