Theorem proving as constraint solving for coherent logic with function symbols
From MaRDI portal
Cites work
- \textsf{Goéland}: a concurrent tableau-based theorem prover (system description)
- A coherent logic based geometry theorem prover capable of producing formal and readable proofs
- A vernacular for coherent logic
- Abductive reasoning. Logical investigations into discovery and explanation
- An abstract decision procedure for a theory of inductive data types.
- An interactive SMT tactic in Coq using abductive reasoning
- Automated completion of statements and proofs in synthetic geometry: an approach based on constraint solving
- Automated generation of illustrated proofs in geometry and beyond
- Automating Coherent Logic
- AVATAR: The Architecture for First-Order Theorem Provers
- CDCL-Based Abstract State Transition System for Coherent Logic
- Encoding First Order Proofs in SAT
- Encoding first order proofs in SMT
- From Tarski to Hilbert
- GCLC -- a tool for constructive Euclidean geometry and more than that
- Geometrisation of first-order logic
- Geometry constructions language
- scientific article; zbMATH DE number 3899653 (Why is no real title available?)
- scientific article; zbMATH DE number 2155188 (Why is no real title available?)
- scientific article; zbMATH DE number 1926614 (Why is no real title available?)
- scientific article; zbMATH DE number 871441 (Why is no real title available?)
- scientific article; zbMATH DE number 1395652 (Why is no real title available?)
- scientific article; zbMATH DE number 3254863 (Why is no real title available?)
- scientific article; zbMATH DE number 3076631 (Why is no real title available?)
- Interactive theorem proving and program development. Coq'Art: the calculus of inductive constructions. Foreword by Gérard Huet and Christine Paulin-Mohring.
- Isabelle/HOL. A proof assistant for higher-order logic
- Mizar: state-of-the-art and beyond
- On the mechanization of the proof of Hessenberg's theorem in coherent logic
- Processes, Terms and Cycles: Steps on the Road to Infinity
- Proof-checking Euclid
- Reducing higher-order theorem proving to a sequence of SAT problems
- Scalable algorithms for abduction via enumerative syntax-guided synthesis
- Theorem proving as constraint solving with coherent logic
- Theorem proving for classical logic with partial functions by reduction to Kleene logic
- URSA: a system for uniform reduction to SAT
This page was built for publication: Theorem proving as constraint solving for coherent logic with function symbols
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q6893591)
