
Z
 Referenced in 274 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 153 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 71 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 107 articles
[sw09685]
 interactive proof development in the natural deduction style. It supports refinement proof as a basic...

TRAMP
 Referenced in 20 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 17 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...

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

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 40 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...

Symlog
 Referenced in 3 articles
[sw32623]
 formal proofs in Fitchstyle natural deduction systems of propositional and predicate logic...

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...

GCLC
 Referenced in 29 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 18 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...