Human-centered automated proof search
type: Item
instance of: scholarly article
title: Human-centered automated proof search
author: Wilfried Sieg
author: Farzaneh Derakhshan
published in: Journal of Automated Reasoning
publication date: 2022-01-21T00:00:00Z
Mathematics Subject Classification ID: 68V15
zbMATH DE Number: 7461268
zbMATH Keywords: proof search
zbMATH Keywords: automated theorem proving
zbMATH Keywords: natural deduction
zbMATH Keywords: natural intercalation calculus
zbMATH Keywords: Fitch diagrams
zbMATH Keywords: normal proofs
zbMATH Keywords: machine-oriented proof methods
describes a project that uses: Mizar
MaRDI profile type: Publication
full work available at URL: s10817-021-09594-z
OpenAlex ID: W3191531957
cites work: Q3880316
cites work: More on the problem of finding a mapping between clause representation and natural-deduction representation
cites work: The role of the Mizar mathematical library for interactive proof development in Mizar
cites work: Non-resolution theorem proving
cites work: Sir Timothy Gowers Interview
cites work: Q5815602
cites work: Q3996619
cites work: A fully automatic theorem prover with human-style output
cites work: Untersuchungen über das logische Schliessen. II
cites work: The consistency of arithmetics
cites work: Q4619818
cites work: Gentzen and Jaśkowski natural deduction: fundamentally similar but importantly different
cites work: Q5772177
cites work: On the rules of suppositions in formal logic
cites work: Q3023557
cites work: The automation of proof: a historical and sociological exploration
cites work: Automated natural deduction in THINKER
cites work: A Brief History of Natural Deduction
cites work: Natural deduction
cites work: Q5559220
cites work: Q4845456
cites work: The AProS Project: Strategic Thinking & Computational Logic
cites work: Q3001104
cites work: Normal natural deduction proofs (in classical logic)
cites work: Mechanizing Mathematical Reasoning
cites work: Automated search for Gödel's proofs
cites work: NATURAL FORMALIZATION: DERIVING THE CANTOR-BERNSTEIN THEOREM IN ZF
cites work: Hilbert's Twenty-Fourth Problem
cites work: Q4499084
cites work: Gentzen's Proof of Normalization for Natural Deduction
cites work: Toward Mechanical Mathematics
DOI: 10.1007/S10817-021-09594-Z
description: scientific article; zbMATH DE number 7461268