Theorem proving as constraint solving with coherent logic (Q2102932): Difference between revisions

@@ Property / MaRDI profile type @@
+MaRDI publication profile
@@ Property / MaRDI profile type: MaRDI publication profile / rank @@
+Normal rank
@@ Property / full work available at URL @@
+https://doi.org/10.1007/s10817-022-09629-z
+Normal rank
@@ Property / OpenAlex ID @@
+W4281252527
@@ Property / OpenAlex ID: W4281252527 / rank @@
+Normal rank
@@ Property / Wikidata QID @@
+Q113901232
@@ Property / Wikidata QID: Q113901232 / rank @@
+Normal rank
@@ Property / cites work @@
+Finding good proofs for description logic entailments using recursive quality measures
+Normal rank
@@ Property / cites work @@
+Automating Resolution is NP-Hard
@@ Property / cites work: Automating Resolution is NP-Hard / rank @@
+Normal rank
@@ Property / cites work @@
+A FORMAL SYSTEM FOR EUCLID’S<i>ELEMENTS</i>
@@ Property / cites work: A FORMAL SYSTEM FOR EUCLID’S<i>ELEMENTS</i> / rank @@
+Normal rank
@@ Property / cites work @@
+Proof-checking Euclid
@@ Property / cites work: Proof-checking Euclid / rank @@
+Normal rank
@@ Property / cites work @@
+Q4665735
@@ Property / cites work: Q4665735 / rank @@
+Normal rank
@@ Property / cites work @@
+Automating Coherent Logic
@@ Property / cites work: Automating Coherent Logic / rank @@
+Normal rank
@@ Property / cites work @@
+On the mechanization of the proof of Hessenberg's theorem in coherent logic
+Normal rank
@@ Property / cites work @@
+Q5503674
@@ Property / cites work: Q5503674 / rank @@
+Normal rank
@@ Property / cites work @@
+Hammering towards QED
@@ Property / cites work: Hammering towards QED / rank @@
+Normal rank
@@ Property / cites work @@
+Automatic Proof and Disproof in Isabelle/HOL
@@ Property / cites work: Automatic Proof and Disproof in Isabelle/HOL / rank @@
+Normal rank
@@ Property / cites work @@
+Semi-intelligible Isar proofs from machine-generated proofs
+Normal rank
@@ Property / cites work @@
+Extending Sledgehammer with SMT solvers
@@ Property / cites work: Extending Sledgehammer with SMT solvers / rank @@
+Normal rank
@@ Property / cites work @@
+More SPASS with Isabelle
@@ Property / cites work: More SPASS with Isabelle / rank @@
+Normal rank
@@ Property / cites work @@
+Encoding First Order Proofs in SMT
@@ Property / cites work: Encoding First Order Proofs in SMT / rank @@
+Normal rank
@@ Property / cites work @@
+Zenon: An Extensible Automated Theorem Prover Producing Checkable Proofs
+Normal rank
@@ Property / cites work @@
+Parallel postulates and continuity axioms: a mechanized study in intuitionistic logic using Coq
+Normal rank
@@ Property / cites work @@
+Fast LCF-Style Proof Reconstruction for Z3
@@ Property / cites work: Fast LCF-Style Proof Reconstruction for Z3 / rank @@
+Normal rank
@@ Property / cites work @@
+Reducing higher-order theorem proving to a sequence of SAT problems
+Normal rank
@@ Property / cites work @@
+The vectorization of ITPACK 2C
@@ Property / cites work: The vectorization of ITPACK 2C / rank @@
+Normal rank
@@ Property / cites work @@
+Inductive logic programming at 30
@@ Property / cites work: Inductive logic programming at 30 / rank @@
+Normal rank
@@ Property / cites work @@
+Practical Proof Search for Coq by Type Inhabitation
+Normal rank
@@ Property / cites work @@
+Hammer for Coq: automation for dependent type theory
+Normal rank
@@ Property / cites work @@
+Encoding First Order Proofs in SAT
@@ Property / cites work: Encoding First Order Proofs in SAT / rank @@
+Normal rank
@@ Property / cites work @@
+GEOMETRISATION OF FIRST-ORDER LOGIC
@@ Property / cites work: GEOMETRISATION OF FIRST-ORDER LOGIC / rank @@
+Normal rank
@@ Property / cites work @@
+Permutability of proofs in intuitionistic sequent calculi
+Normal rank
@@ Property / cites work @@
+A fully automatic theorem prover with human-style output
+Normal rank
@@ Property / cites work @@
+Conflict-Driven Answer Set Enumeration
@@ Property / cites work: Conflict-Driven Answer Set Enumeration / rank @@
+Normal rank
@@ Property / cites work @@
+URSA: A System for Uniform Reduction to SAT
@@ Property / cites work: URSA: A System for Uniform Reduction to SAT / rank @@
+Normal rank
@@ Property / cites work @@
+Q4874803
@@ Property / cites work: Q4874803 / rank @@
+Normal rank
@@ Property / cites work @@
+The area method. A recapitulation
@@ Property / cites work: The area method. A recapitulation / rank @@
+Normal rank
@@ Property / cites work @@
+A review and prospect of readable machine proofs for geometry theorems
+Normal rank
@@ Property / cites work @@
+HOL(y)Hammer: online ATP service for HOL Light
@@ Property / cites work: HOL(y)Hammer: online ATP service for HOL Light / rank @@
+Normal rank
@@ Property / cites work @@
+Proof simplification and automated theorem proving
+Normal rank
@@ Property / cites work @@
+Q5813181
@@ Property / cites work: Q5813181 / rank @@
+Normal rank
@@ Property / cites work @@
+iProver – An Instantiation-Based Theorem Prover for First-Order Logic (System Description)
+Normal rank
@@ Property / cites work @@
+On preprocessing techniques and their impact on propositional model counting
+Normal rank
@@ Property / cites work @@
+Sheaves in geometry and logic: a first introduction to topos theory
+Normal rank
@@ Property / cites work @@
+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
+Normal rank
@@ Property / cites work @@
+Short Proofs Are Hard to Find
@@ Property / cites work: Short Proofs Are Hard to Find / rank @@
+Normal rank
@@ Property / cites work @@
+Isabelle/HOL. A proof assistant for higher-order logic
+Normal rank
@@ Property / cites work @@
+Subsumption Algorithms for Three-Valued Geometric Resolution
+Normal rank
@@ Property / cites work @@
+Geometric Resolution: A Proof Procedure Based on Finite Model Search
+Normal rank
@@ Property / cites work @@
+IeanCOP: lean connection-based theorem proving
@@ Property / cites work: IeanCOP: lean connection-based theorem proving / rank @@
+Normal rank
@@ Property / cites work @@
+Isabelle. A generic theorem prover
@@ Property / cites work: Isabelle. A generic theorem prover / rank @@
+Normal rank
@@ Property / cites work @@
+Local Search for Unsatisfiability
@@ Property / cites work: Local Search for Unsatisfiability / rank @@
+Normal rank
@@ Property / cites work @@
+Reliable reconstruction of fine-grained proofs in a proof assistant
+Normal rank
@@ Property / cites work @@
+Interlude: About the First Theorem
@@ Property / cites work: Interlude: About the First Theorem / rank @@
+Normal rank
@@ Property / cites work @@
+A Vernacular for Coherent Logic
@@ Property / cites work: A Vernacular for Coherent Logic / rank @@
+Normal rank
@@ Property / cites work @@
+A Coherent Logic Based Geometry Theorem Prover Capable of Producing Formal and Readable Proofs
+Normal rank
@@ Property / cites work @@
+The TPTP World – Infrastructure for Automated Reasoning
+Normal rank
@@ Property / cites work @@
+Hilbert's twenty-fourth problem
@@ Property / cites work: Hilbert's twenty-fourth problem / rank @@
+Normal rank
@@ Property / cites work @@
+ATP and presentation service for Mizar formalizations
+Normal rank
@@ Property / cites work @@
+Finding shortest proofs: An application of linked inference rules
+Normal rank
@@ Property / cites work @@
+AVATAR: The Architecture for First-Order Theorem Provers
+Normal rank
@@ Property / cites work @@
+Types for Proofs and Programs
@@ Property / cites work: Types for Proofs and Programs / rank @@
+Normal rank
@@ Property / cites work @@
+Automating the search for elegant proofs
@@ Property / cites work: Automating the search for elegant proofs / rank @@
+Normal rank
@@ Property / cites work @@
+Q3624141
@@ Property / cites work: Q3624141 / rank @@
+Normal rank