| http://dbpedia.org/ontology/abstract
|
In logic and mathematics, a formal proof o … In logic and mathematics, a formal proof or derivation is a finite sequence of sentences (called well-formed formulas in the case of a formal language), each of which is an axiom, an assumption, or follows from the preceding sentences in the sequence by a rule of inference. It differs from a natural language argument in that it is rigorous, unambiguous and mechanically verifiable. If the set of assumptions is empty, then the last sentence in a formal proof is called a theorem of the formal system. The notion of theorem is not in general effective, therefore there may be no method by which we can always find a proof of a given sentence or determine that none exists. The concepts of Fitch-style proof, sequent calculus and natural deduction are generalizations of the concept of proof. The theorem is a syntactic consequence of all the well-formed formulas preceding it in the proof. For a well-formed formula to qualify as part of a proof, it must be the result of applying a rule of the deductive apparatus (of some formal system) to the previous well-formed formulas in the proof sequence. Formal proofs often are constructed with the help of computers in interactive theorem proving (e.g., through the use of proof checker and automated theorem prover). Significantly, these proofs can be checked automatically, also by computer. Checking formal proofs is usually simple, while the problem of finding proofs (automated theorem proving) is usually computationally intractable and/or only semi-decidable, depending upon the formal system in use., depending upon the formal system in use.
, البرهان (بالإنجليزية: Proof) في الفلسفة أ … البرهان (بالإنجليزية: Proof) في الفلسفة أو المنطق هو عملية استدلال تهدف إلى تأكيد الصدق (أو الكذب) في قضية ما. والاستدلالات التي يبنى عليها البرهان، والتي تترتب عليها القضية منطقياً تسمى الحجج. ويفترض في الحجج أنها صادقة ولا تتضمن مقدمات تفترض القضية المراد البرهنة عليها، وإلا كانت النتيجة مصادرة على المطلوب. والبرهان الذي يقيم صدق القضية يسمى برهاناً فحسب، أما البرهان الذي يقيم كذب القضية فيسمى تفنيداً.لبرهان الذي يقيم كذب القضية فيسمى تفنيداً.
, La dimostrazione è una serie di ragionamenti logici che, partendo da una ipotesi, porta necessariamente a una tesi. Consiste nel verificare, nel senso di mostrarne la ragionevole verità, un predicato, una frase.
, Em lógica, uma derivação formal (ou prova … Em lógica, uma derivação formal (ou prova formal) é uma sequência finita de sentenças onde cada sentença pode ser um axioma ou então pode ser obtida como consequência direta de sentenças anteriores na sequência utilizando-se uma regra de inferência. A última sentença na sequência é um teorema do sistema formal. A noção de teorema não é em geral efetiva, pois pode não haver um método através do qual nós possamos sempre encontrar uma derivação de uma dada sentença ou determinar que não existe nenhuma derivação. O conceito de dedução é uma generalização do conceito de derivação. O teorema é uma de todas as fórmulas bem formadas (fbf) precedidas na derivação. Para uma fbf fazer parte de uma derivação, ela deve ser resultado da aplicação de uma regra do sistema dedutivo de algum sistema formal nas fbfs anteriores na sequência da derivação. As derivações formais muitas vezes são construídas com a ajuda de computadores através da . É interessante notar que tais derivações podem ser conferidas automaticamente com o uso do computador. Conferir derivações formais normalmente é uma tarefa trivial, enquanto que encontrar tais derivações (demonstração automática de teoremas) geralmente é bastante difícil.e teoremas) geralmente é bastante difícil.
, En lógica, una derivación formal (o prueba … En lógica, una derivación formal (o prueba formal) es una secuencia finita de sentencias donde cada sentencia puede ser un axioma o puede ser obtenida como consecuencia directa de las sentencias anteriores en la secuencia utilizándose una regla de inferencia. La última frase siguiente es un teorema del sistema formal. La noción del teorema no es efectiva en general, porque no puede haber un método mediante el cual siempre podemos encontrar una derivación de una resolución dictada o determinar que no hay derivación. El concepto de deducción es una generalización del concepto de derivación. El teorema es una de todas las fórmulas bien formadas (fbf) precedidas en la derivación. Para una parte fbf de una unión, ella debe ser el resultado de aplicar una regla de sistema deductivo de cualquier sistema formal previa en fbfs siguiente derivación. Las derivaciones formales muchas veces se construye con la ayuda de ordenadores a través de la demostración interactiva de teoremas. Resulta interesante notar que estas derivaciones pueden ser conferidas automáticamente con el uso del ordenador. Conferir derivaciones formales suele ser una tarea trivial, mientras que encontrar tales derivaciones (demostración automática de teoremas) suele ser bastante difícil.a de teoremas) suele ser bastante difícil.
, Доказ, доведення — визначення істинності т … Доказ, доведення — визначення істинності твердження шляхом встановлення його необхідного зв'язку з іншими твердженнями, прийнятими за істинні. Доведення полягає у висуненні тези (положення, що доводиться), всіх інших можливих гіпотез і підшукуванні аргументів — істинних тверджень, що впливають на ймовірність гіпотез. Доведення закінчене, якщо жодна гіпотеза, крім тези, неможлива. Доведення буває пряме, якщо істинність тези безпосередньо випливає з аргументів, і непряме, якщо доводиться хибність альтернативних гіпотез. Поняття Доведення для кожної теорії вказує на способи, якими аргументи пов'язуються з гіпотезами, й залежить від характеру знань, підсумованих у теорії. Встановлювані формальною логікою правила Доведення загальнозначимі лише в тому розумінні, що порушення їх неприпустиме. Доведення є суто формально-логічним, якщо теза доводиться тільки засобами формальної логіки. Таке Доведення вимагає формулювання тез формалізованою мовою логіки у вигляді правильно побудованих формул (п. п. ф.). Тоді при аксіоматичній побудові Доведенням називається скінченна послідовність, що складається з однієї або більше п. п. ф., якщо кожна п. п. ф. в послідовності є або аксіомою, або безпосередньо виводиться за одним з правил виводу з попередніх п. п. ф. послідовностей. Доведення пов'язане з практикою, яка визначає не тільки істинність аргумента, а й передумови його застосування й використання в розвитку наукових знань. й використання в розвитку наукових знань.
, Formeel bewijs in de formele wetenschap is … Formeel bewijs in de formele wetenschap is een eindige reeks proposities ( in formele taal) binnen het kader van de beschrijving van formele systemen waarbij elke propositie door middel van afleidingsregels uit voorafgaande proposities of axiomas kan worden afgeleid. De uiteindelijke propositie is een stelling. Het afleiden van een stelling is een logisch gevolg van de voorafgaande formules. Een logische consequentie is het resultaat van het deductieve systeem van een formeel systeem. Bij wordt formeel bewijs geleverd en gecontroleerd met behulp van computers. Het eerste wordt ook wel het genoemd en is vanzelfsprekend moeilijker dan het laatste.anzelfsprekend moeilijker dan het laatste.
, Une démonstration formelle est une séquenc … Une démonstration formelle est une séquence finie de propositions (appelées formules bien formées dans le cas d'un langage formel) dont chacun est un axiome, une hypothèse, ou résulte des propositions précédentes dans la séquence par une règle d'inférence. La dernière proposition de la séquence est un théorème d'un système formel. La notion de théorème n'est en général pas effective, donc n'existe pas de méthode par laquelle nous pouvons à chaque fois trouver une démonstration d'une proposition donnée ou de déterminer s'il y en a une. Le concept de déduction naturelle est une généralisation de la notion de démonstration. Le théorème est une conséquence syntaxique de toutes les formules bien formées qui la précèdent dans la démonstration. Pour qu'une formule bien formée soit présente dans le cadre d'une démonstration, elle doit être le résultat de l'application d'une règle de l'appareil déductif. Les démonstration formelles sont souvent construits à l'aide d'ordinateurs en tant qu'assistants de preuve. De manière significative, ces preuves peuvent être vérifiées automatiquement, également par ordinateur. La vérification des démonstrations formelles est généralement simple, alors que trouver des démonstrations (démonstration automatique de théorèmes) est généralement informatiquement intraitable et/ou seulement semi-décidable, selon le système formel utilisé.écidable, selon le système formel utilisé.
|
| http://dbpedia.org/ontology/wikiPageExternalLink
|
https://www.isa-afp.org/ +
, https://web.archive.org/web/20090908075745/http:/2piix.com/articles/title/Logic/ +
, https://www.ams.org/notices/200811/%7Cwork=Notices +
, http://mizar.org/ +
|
| http://dbpedia.org/ontology/wikiPageID
|
1197184
|
| http://dbpedia.org/ontology/wikiPageInterLanguageLink
|
http://de.dbpedia.org/resource/Axiomatischer_Beweis +
|
| http://dbpedia.org/ontology/wikiPageLength
|
5200
|
| http://dbpedia.org/ontology/wikiPageRevisionID
|
1113095164
|
| http://dbpedia.org/ontology/wikiPageWikiLink
|
http://dbpedia.org/resource/Rule_of_inference +
, http://dbpedia.org/resource/Proof_assistant +
, http://dbpedia.org/resource/Proposition_%28philosophy%29 +
, http://dbpedia.org/resource/Reference +
, http://dbpedia.org/resource/Follows_from +
, http://dbpedia.org/resource/Sequence_%28mathematics%29 +
, http://dbpedia.org/resource/Semantics +
, http://dbpedia.org/resource/Mathematical_proof +
, http://dbpedia.org/resource/Generalization +
, http://dbpedia.org/resource/Category:Proof_theory +
, http://dbpedia.org/resource/Set_%28mathematics%29 +
, http://dbpedia.org/resource/Proof_calculus +
, http://dbpedia.org/resource/Computationally_intractable +
, http://dbpedia.org/resource/Natural_deduction +
, http://dbpedia.org/resource/Logic +
, http://dbpedia.org/resource/Semi-decidable +
, http://dbpedia.org/resource/Interactive_theorem_proving +
, http://dbpedia.org/resource/Mathematics +
, http://dbpedia.org/resource/Category:Syntax_%28logic%29 +
, http://dbpedia.org/resource/Well-formed_formula +
, http://dbpedia.org/resource/Symbol +
, http://dbpedia.org/resource/Category:Logical_truth +
, http://dbpedia.org/resource/Formal_language +
, http://dbpedia.org/resource/Theorem +
, http://dbpedia.org/resource/Interpretation_%28logic%29 +
, http://dbpedia.org/resource/Structure_%28mathematical_logic%29 +
, http://dbpedia.org/resource/De_Bruijn_Factor +
, http://dbpedia.org/resource/Automated_theorem_prover +
, http://dbpedia.org/resource/Category:Formal_systems +
, http://dbpedia.org/resource/Fitch_notation +
, http://dbpedia.org/resource/Alphabet +
, http://dbpedia.org/resource/Effective_method +
, http://dbpedia.org/resource/Formal_semantics_%28logic%29 +
, http://dbpedia.org/resource/Deductive_apparatus +
, http://dbpedia.org/resource/Sequence +
, http://dbpedia.org/resource/Proof_%28truth%29 +
, http://dbpedia.org/resource/Axiom +
, http://dbpedia.org/resource/Formal_system +
, http://dbpedia.org/resource/Axiomatic_system +
, http://dbpedia.org/resource/Sequent_calculus +
, http://dbpedia.org/resource/Formal_verification +
, http://dbpedia.org/resource/Category:Formal_languages +
, http://dbpedia.org/resource/Meaning_%28linguistics%29 +
, http://dbpedia.org/resource/Transformation_rule +
, http://dbpedia.org/resource/String_%28computer_science%29 +
, http://dbpedia.org/resource/Proof_theory +
|
| http://dbpedia.org/property/wikiPageUsesTemplate
|
http://dbpedia.org/resource/Template:Mathematical_logic +
, http://dbpedia.org/resource/Template:Main +
, http://dbpedia.org/resource/Template:Short_description +
, http://dbpedia.org/resource/Template:Authority_control +
, http://dbpedia.org/resource/Template:Cite_web +
, http://dbpedia.org/resource/Template:Logical_truth +
, http://dbpedia.org/resource/Template:Reflist +
|
| http://purl.org/dc/terms/subject
|
http://dbpedia.org/resource/Category:Formal_systems +
, http://dbpedia.org/resource/Category:Proof_theory +
, http://dbpedia.org/resource/Category:Formal_languages +
, http://dbpedia.org/resource/Category:Syntax_%28logic%29 +
, http://dbpedia.org/resource/Category:Logical_truth +
|
| http://purl.org/linguistics/gold/hypernym
|
http://dbpedia.org/resource/Sequence +
|
| http://www.w3.org/ns/prov#wasDerivedFrom
|
http://en.wikipedia.org/wiki/Formal_proof?oldid=1113095164&ns=0 +
|
| http://xmlns.com/foaf/0.1/isPrimaryTopicOf
|
http://en.wikipedia.org/wiki/Formal_proof +
|
| owl:sameAs |
http://fr.dbpedia.org/resource/D%C3%A9monstration_formelle +
, http://rdf.freebase.com/ns/m.043v063 +
, http://yago-knowledge.org/resource/Formal_proof +
, http://www.wikidata.org/entity/Q2762418 +
, http://es.dbpedia.org/resource/Prueba_formal +
, http://nl.dbpedia.org/resource/Formeel_bewijs +
, http://ar.dbpedia.org/resource/%D8%A8%D8%B1%D9%87%D8%A7%D9%86_%D9%81%D9%84%D8%B3%D9%81%D9%8A +
, http://uk.dbpedia.org/resource/%D0%94%D0%BE%D0%BA%D0%B0%D0%B7_%28%D0%BB%D0%BE%D0%B3%D1%96%D0%BA%D0%B0%29 +
, http://it.dbpedia.org/resource/Dimostrazione +
, https://global.dbpedia.org/id/2a5Bq +
, http://pt.dbpedia.org/resource/Deriva%C3%A7%C3%A3o_formal +
, http://dbpedia.org/resource/Formal_proof +
|
| rdf:type |
http://dbpedia.org/class/yago/Communication100033020 +
, http://dbpedia.org/class/yago/Argument106648724 +
, http://dbpedia.org/class/yago/Abstraction100002137 +
, http://dbpedia.org/class/yago/Language106282651 +
, http://dbpedia.org/class/yago/Evidence106643408 +
, http://dbpedia.org/class/yago/Indication106797169 +
, http://dbpedia.org/class/yago/MathematicalProof106647864 +
, http://dbpedia.org/class/yago/Proof106647614 +
, http://dbpedia.org/class/yago/WikicatMathematicalProofs +
, http://dbpedia.org/class/yago/WikicatFormalLanguages +
|
| rdfs:comment |
البرهان (بالإنجليزية: Proof) في الفلسفة أ … البرهان (بالإنجليزية: Proof) في الفلسفة أو المنطق هو عملية استدلال تهدف إلى تأكيد الصدق (أو الكذب) في قضية ما. والاستدلالات التي يبنى عليها البرهان، والتي تترتب عليها القضية منطقياً تسمى الحجج. ويفترض في الحجج أنها صادقة ولا تتضمن مقدمات تفترض القضية المراد البرهنة عليها، وإلا كانت النتيجة مصادرة على المطلوب. والبرهان الذي يقيم صدق القضية يسمى برهاناً فحسب، أما البرهان الذي يقيم كذب القضية فيسمى تفنيداً.لبرهان الذي يقيم كذب القضية فيسمى تفنيداً.
, Une démonstration formelle est une séquenc … Une démonstration formelle est une séquence finie de propositions (appelées formules bien formées dans le cas d'un langage formel) dont chacun est un axiome, une hypothèse, ou résulte des propositions précédentes dans la séquence par une règle d'inférence. La dernière proposition de la séquence est un théorème d'un système formel. La notion de théorème n'est en général pas effective, donc n'existe pas de méthode par laquelle nous pouvons à chaque fois trouver une démonstration d'une proposition donnée ou de déterminer s'il y en a une. Le concept de déduction naturelle est une généralisation de la notion de démonstration.éralisation de la notion de démonstration.
, En lógica, una derivación formal (o prueba … En lógica, una derivación formal (o prueba formal) es una secuencia finita de sentencias donde cada sentencia puede ser un axioma o puede ser obtenida como consecuencia directa de las sentencias anteriores en la secuencia utilizándose una regla de inferencia. La última frase siguiente es un teorema del sistema formal. La noción del teorema no es efectiva en general, porque no puede haber un método mediante el cual siempre podemos encontrar una derivación de una resolución dictada o determinar que no hay derivación. El concepto de deducción es una generalización del concepto de derivación.generalización del concepto de derivación.
, In logic and mathematics, a formal proof o … In logic and mathematics, a formal proof or derivation is a finite sequence of sentences (called well-formed formulas in the case of a formal language), each of which is an axiom, an assumption, or follows from the preceding sentences in the sequence by a rule of inference. It differs from a natural language argument in that it is rigorous, unambiguous and mechanically verifiable. If the set of assumptions is empty, then the last sentence in a formal proof is called a theorem of the formal system. The notion of theorem is not in general effective, therefore there may be no method by which we can always find a proof of a given sentence or determine that none exists. The concepts of Fitch-style proof, sequent calculus and natural deduction are generalizations of the concept of proof.e generalizations of the concept of proof.
, La dimostrazione è una serie di ragionamenti logici che, partendo da una ipotesi, porta necessariamente a una tesi. Consiste nel verificare, nel senso di mostrarne la ragionevole verità, un predicato, una frase.
, Formeel bewijs in de formele wetenschap is … Formeel bewijs in de formele wetenschap is een eindige reeks proposities ( in formele taal) binnen het kader van de beschrijving van formele systemen waarbij elke propositie door middel van afleidingsregels uit voorafgaande proposities of axiomas kan worden afgeleid. De uiteindelijke propositie is een stelling. Het afleiden van een stelling is een logisch gevolg van de voorafgaande formules. Een logische consequentie is het resultaat van het deductieve systeem van een formeel systeem.eductieve systeem van een formeel systeem.
, Em lógica, uma derivação formal (ou prova … Em lógica, uma derivação formal (ou prova formal) é uma sequência finita de sentenças onde cada sentença pode ser um axioma ou então pode ser obtida como consequência direta de sentenças anteriores na sequência utilizando-se uma regra de inferência. A última sentença na sequência é um teorema do sistema formal. A noção de teorema não é em geral efetiva, pois pode não haver um método através do qual nós possamos sempre encontrar uma derivação de uma dada sentença ou determinar que não existe nenhuma derivação. O conceito de dedução é uma generalização do conceito de derivação.ma generalização do conceito de derivação.
, Доказ, доведення — визначення істинності т … Доказ, доведення — визначення істинності твердження шляхом встановлення його необхідного зв'язку з іншими твердженнями, прийнятими за істинні. Доведення полягає у висуненні тези (положення, що доводиться), всіх інших можливих гіпотез і підшукуванні аргументів — істинних тверджень, що впливають на ймовірність гіпотез. Доведення закінчене, якщо жодна гіпотеза, крім тези, неможлива. Доведення буває пряме, якщо істинність тези безпосередньо випливає з аргументів, і непряме, якщо доводиться хибність альтернативних гіпотез. Поняття Доведення для кожної теорії вказує на способи, якими аргументи пов'язуються з гіпотезами, й залежить від характеру знань, підсумованих у теорії. Встановлювані формальною логікою правила Доведення загальнозначимі лише в тому розумінні, що порушення їх неприпустиме. Довзумінні, що порушення їх неприпустиме. Дов
|
| rdfs:label |
Formal proof
, Доказ (логіка)
, Prueba formal
, Dimostrazione
, برهان فلسفي
, Derivação formal
, Démonstration formelle
, Formeel bewijs
|
