
Z
 Referenced in 270 articles
[sw10291]
 with the exception of the natural deduction calculus, see below  only introduction ... broad and tedious exposition of the natural deduction calculus, which is not used further...

ETPS
 Referenced in 149 articles
[sw06302]
 theories in a wide variety of disciplines, deductive information systems for these disciplines, expert systems ... expansion proofs, translating these into natural deduction proofs, constructing natural deduction proofs, translating natural deduction ... interactive facilities of TPS for constructing natural deduction proofs have been used under the name...

TPS
 Referenced in 68 articles
[sw00973]
 theories in a wide variety of disciplines, deductive information systems for these disciplines, expert systems ... expansion proofs, translating these into natural deduction proofs, constructing natural deduction proofs, translating natural deduction...

LEGO
 Referenced in 105 articles
[sw09685]
 interactive proof development in the natural deduction style. It supports refinement proof as a basic...

TRAMP
 Referenced in 19 articles
[sw21343]
 Transformation of MachineFound Proofs into Natural Deduction Proofs at the Assertion Level. The Tramp ... first order logic with equality into natural deduction proofs at the assertion level. Through this...

MUltlog
 Referenced in 15 articles
[sw06604]
 produces a sequent calculus, a natural deduction system, and clause formation rules for this logic...

Pandora
 Referenced in 9 articles
[sw01306]
 Pandora (Proof Assistant for Natural Deduction using Organised Rectangular Areas) is a learning support tool ... designed to guide the construction of natural deduction proofs...

AFFIRM
 Referenced in 6 articles
[sw28906]
 AFFIRM theorem prover is an interative, naturaldeduction system centered around abstract data types. Since...

PROVERB
 Referenced in 4 articles
[sw29672]
 abstracts machinefound proofs to natural deduction style proofs at an adequate level of abstraction...

FOL Fitting
 Referenced in 4 articles
[sw28611]
 semantics, the model existence theorem, a natural deduction proof calculus together with a proof...

KeYmaera
 Referenced in 34 articles
[sw03709]
 verification tool for hybrid systems that combines deductive, real algebraic, and computer algebraic prover technologies ... automated and interactive theorem prover for a natural specification and verification logic for hybrid systems...

ANDP
 Referenced in 1 article
[sw29686]
 Automated natural deduction prover and experiments. The paper presents the heuristics and techniques which ... used to implement automated natural deduction prover (ANDP), the natural deduction was adapted from Gentzen...

Psyche
 Referenced in 2 articles
[sw28518]
 inference rules of the logic in natural deduction: it uses instead a focused sequent calculus...

GCLC
 Referenced in 28 articles
[sw00326]
 storing mathematical contents of visual nature in textual form. In GCLC, there is a build ... links visual and semantical geometrical information with deductive properties and machinegenerated proofs...

Delphin
 Referenced in 16 articles
[sw21365]
 Delphin: Functional programming with deductive systems. We present the design and implementation of the strict ... proofs and typing derivations in a natural and intuitive...

KEIM
 Referenced in 1 article
[sw19608]
 those who want to build or use deduction systems (such as resolution theorem provers) without ... substitutions; proofs, including resolution and natural deduction styles...

TILT
 Referenced in 1 article
[sw24052]
 term represents a proof in the natural deduction calculus. Since the search space...

EUODHILOS
 Referenced in 2 articles
[sw24045]
 tree structured forms of the natural deductionlike style...

MaLARea
 Referenced in 40 articles
[sw10278]
 Reasoning) is a simple metasystem iteratively combining deductive Automated Reasoning tools ... poses quite interesting questions about the nature of thinking, in particular, about...