Theorem proving as constraint solving with coherent logic
From MaRDI portal
Publication:2102932
Recommendations
Cites work
- scientific article; zbMATH DE number 2155188 (Why is no real title available?)
- scientific article; zbMATH DE number 871441 (Why is no real title available?)
- scientific article; zbMATH DE number 5493266 (Why is no real title available?)
- scientific article; zbMATH DE number 3074068 (Why is no real title available?)
- A FORMAL SYSTEM FOR EUCLID’SELEMENTS
- A coherent logic based geometry theorem prover capable of producing formal and readable proofs
- A fully automatic theorem prover with human-style output
- A review and prospect of readable machine proofs for geometry theorems
- A vernacular for coherent logic
- ATP and presentation service for Mizar formalizations
- AVATAR: The Architecture for First-Order Theorem Provers
- An introduction to Gödel's theorems
- Automatic proof and disproof in Isabelle/HOL
- Automating Coherent Logic
- Automating resolution is NP-hard
- Automating the search for elegant proofs
- Conflict-Driven Answer Set Enumeration
- Encoding First Order Proofs in SAT
- Encoding first order proofs in SMT
- Extending Sledgehammer with SMT solvers
- Fast LCF-Style Proof Reconstruction for Z3
- Finding good proofs for description logic entailments using recursive quality measures
- Finding shortest proofs: An application of linked inference rules
- Geometric Resolution: A Proof Procedure Based on Finite Model Search
- Geometrisation of first-order logic
- HOL(y)Hammer: online ATP service for HOL Light
- Hammer for Coq: automation for dependent type theory
- Hammering towards QED
- Hilbert's twenty-fourth problem
- IeanCOP: lean connection-based theorem proving
- Inductive logic programming at 30
- Isabelle. A generic theorem prover
- Isabelle/HOL. A proof assistant for higher-order logic
- Local Search for Unsatisfiability
- More SPASS with Isabelle
- On preprocessing techniques and their impact on propositional model counting
- On the mechanization of the proof of Hessenberg's theorem in coherent logic
- Parallel postulates and continuity axioms: a mechanized study in intuitionistic logic using Coq
- Permutability of proofs in intuitionistic sequent calculi
- Practical Proof Search for Coq by Type Inhabitation
- Proof simplification and automated theorem proving
- Proof-checking Euclid
- Reducing higher-order theorem proving to a sequence of SAT problems
- Reliable reconstruction of fine-grained proofs in a proof assistant
- SATzilla: portfolio-based algorithm selection for SAT
- Semi-intelligible Isar proofs from machine-generated proofs
- Sheaves in geometry and logic: a first introduction to topos theory
- Short Proofs Are Hard to Find
- The TPTP World -- infrastructure for automated reasoning
- The area method. A recapitulation
- The vectorization of ITPACK 2C
- 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
- Types for Proofs and Programs
- URSA: a system for uniform reduction to SAT
- Zenon: An Extensible Automated Theorem Prover Producing Checkable Proofs
- iProver – An Instantiation-Based Theorem Prover for First-Order Logic (System Description)
Cited in
(6)- scientific article; zbMATH DE number 1222430 (Why is no real title available?)
- 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
- Automated generation of illustrated proofs in geometry and beyond
- A vernacular for coherent logic
- scientific article; zbMATH DE number 1285157 (Why is no real title available?)
Describes a project that uses
Uses Software
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)
