35016121
Description
Flashcards by Simone Andreozzi, updated more than 1 year ago
|
Created by Simone Andreozzi
almost 3 years ago
|
|
| Question | Answer |
| cos'è una proposizione logica? | una proposizione formata unicamente da concetti logici è detta proposizione logica |
| cos'è una dimostrazione logica | una dimostrazione di una proposizione A ottenuta soltanto attraverso regole logiche è detta dimostrazione logica di A |
| cos'è una dimostrazione di una conclusione A da un'ipotesi B? | anche detta derivazione da A a B, ragionamento o argomentazione da A a B. Ogni singolo passo compiuto per ricavare la conclusione A dall'ipotesi B |
| Cos'è un dibattito | dibattiti o dispute sono dei "giochi" di proposizioni, dove un proponente propone appunto una proposizione A e l'opponente invece contrappone una proposizione B(contraddittoria). la discussione avviene tramite mosse di proponente e opponente |
| La dimostrazione di A da B è uguale alla dimostrazione del duale logico di B dal duale logico di A? | sì, in quanto ogni dimostrazione di A da B, corrisponde ad una refutazione di B da A creando un una proposizione logicamente duale, dove A è anche detta duale logico di B e vice versa |
| Quali sono i principali concetti logici sulle classi? | inclusione: classe X contenuta in classe Y separazione: classe X non contenuta in classe Y condivisione: classe X e classe Y condividono elementi esterno: la classe X ha elementi esterni alla classe Y finito o infinito: "la classe X è finita" e la sua negazione "la classe X è infinita" |
| Cos'è una classe ordinata? | la classe ordinata è una classe che ha un ordine ben definito all'interno di n elementi disposti in fila |
| Cos'è il dominio e cos'è il codominio di un'operazione? | in un passaggio dalla classe X alla classe Y, il dominio sono tutti gli elementi di una classe X o classe di partenza e il codominio sono tutti gli elementi di X che diventeranno di Y o classe di arrivo |
| Cos'è una strategia sequenziale e cos'è una strategia non-sequenziale? | una strategia sequenziale è una strategia che può essere eseguita da un singolo soggetto, al contrario, una strategia non-sequenziale è una strategia che ha bisogno della cooperazione o l'intervento di più soggetti |
| Cos'è l'organizzazione assiomatica di una teoria? | teoria assiomatica. Una organizzazione assiomatica delle proposizioni e dei concetti di una disciplina scientifica -Si fissa un piccolo numero finiti di proposizioni chiamate assiomi -Si fissa un piccolo numero finito di concetti chiamati concetti primitivi -Negli assiomi abbiamo solo concetti primitivi e logici -I teoremi della disciplina sono conclusioni di dimostrazioni logiche di assiomi -Tutti i concetti noti della disciplina si ottengono mediante definizioni dai concetti primitivi e logici |
| Cosa si intende dicendo che la concezione classica delle proposizioni è bivalente? | si intende che gli unici valori delle proposizioni sono vero o falso |
| Cosa si intende dicendo che la concezione classica delle proposizioni è atemporale ed aspaziale? | i valori delle proposizioni sono atemporali e aspaziali quindi non correlati all'ordine di tempo e di spazio nel quale sono collocati. Il valore delle proposizioni è indipendente dal tempo |
| Cos'è il principio dell'interazione tra una proposizione e la sua negazione classica? | un principio secondo il quale partendo dalla proposizione e la sua negazione classica, si ottiene automaticamente il soddisfacimento dei 4 principi fondamentali della logica classica: interazione(+,-), terzo escluso(+,- o -,+), non contraddizione (no -,- o +,+) e di identità se + allora -) |
| Quali sono i 4 principi fondamentali della logica classica? | 4 principi fondamentali della logica classica: interazione(+,-), terzo escluso(+,- o -,+), non contraddizione (no -,- o +,+) e di identità se + allora -) |
| modus ponens? | partendo da una dimostrazione di B dall'ipotesi A, se A è vera e c'è una dimostraizone di B da A, allora anche B è vera |
| modus tollens? | partendo da una dimostrazione di B dall'ipotesi A. Se B è falsa e c'è una dimostrazione di B da A, allora A è falsa |
| Cos'è la regola del taglio? | regola del taglio o regola di della comunicazione input/output la composizione di due dimostrazioni dove A in una proposizione è conclusione e nell'altra è ipotesi produce una dimostrazione dove l'ipotesi B che dipende da A della prima dimostrazione genererà una conclusione C che discende da A |
| Che cos'è la regola della consequetia mirabilis o regola della contrazione? | E' una regola di dimostrazione tipica dela logica classica, afferma che se c'è una dimostrazione di A a partire dalla sua negazione, allora c'è una dimostrazione di A. È detta Consequetia Mirabilis perché permette di concludere la verità di una proposizione in maniera straordinaria, derivando cioè dalla sua negazione |
| Cos'è la regola dell'A fortiori o regola dell'indebolimento? | se c'è una dimostrazione di B allora c'è una dimostrazione di B da A dove A è una qualunque proposizione Viene chiamata A fortiori perché permette di concludere che una proposizione B discende da una proposizione A poiché a fortiori si è gia dimostrata la proposizione di B |
| Che cos'è la concezione estensionale e la concezione vero-funzionale dei connettivi? | In Logica Classica, il valore della proposizione ottenuta da A a B mediante un connettivo, dipende esclusivamente dal valore di verità di A e di B. Questa concezione dei connettivi propria della logica classica, viene detta estensionale, in quanto si occupa soltanto del valore delle proposizioni, è vero funzionale, in quanto questo valore viene fatto dipendere unicamente dai valore delle sue proposizioni |
| la tavola dei connettivi della logica classica | e:^ oppure:V se ... allora:--> se e soltanto se:<--> |
| Definisci l'implicazione classica a partire dalla disgiunzione classica e dalla negazione classica | traducendo in logica classica la frase "se A allora B"(-->), l'unica situazione di falsità è quando A è vera e B è falsa, altrimenti sono tutte vere secondo la logica classica. la formula A --> può essere scomposta in ¬A V B |
| Definisci l'alternativa classica e l'equivalenza classica a partire dalla congiunzione classica, dalla disgiunzione classica(oppure) e dalla negazione classica | TROVA LA RISPOSTA |
| Enuncia le regole della negazione delle proposizioni ottenute mediante i connettivi principali | La negazione classica di una congiunzione classica di due proposizioni è la disgiunzione classica delle negazioni classiche delle due proposizioni. La negazione classica di una disgiunzione classica di due proposizioni è la congiunzione classica delle negazioni classiche delle due proposizioni. La congiunzione classica e la disgiunzione classica sono connettivi duali La negazione classica dell'implicazione classica di due proposizioni è la congiunzione classica tra le proposizioni stesse La negazione di un'equivalenza classica tra le due proposizioni è l'alternativa classica tra le proposizioni stesse |
| Qual è la regola per ottenere una dimostrazione di una congiunzione classica? Quali sono le regole per usare in una dimostrazione una congiunzione classica? | DALLA VERITÀ A E DALLA VERITÀ B POSSIAMO CONCLUDERE LA VERITÀ DI A V B per dimostrare una congiunzione classica bisogna assegnare 1 come valore alla congiunzione ciò significa che entrambe le proposizioni devono avere valore 1 e quindi 4 dimostrazioni |
| Qual è la regola per ottenere una dimostrazione di una disgiunzione classica? Quali sono le regole per usare in una dimostrazione una disgiunzione classica? | DALLA VERITÀ DI A E DALLA FALSITÀ DI B POSSIAMO DIMOSTRARE LA DISGIUNZIONE Per essere dimostrata la disgiunzione, gli diamo il valore 1, per avere il valore 1, una delle due proposizioni deve essere 1 e quindi, partendo dal presupposto che se una è vera l'altra deve essere falsa, avremo per forza almeno una proposizione dimostrata, vera o falsa che ci darà la verifica del contrario |
| Quali sono i principali tipi logici? | Il tipo logico consiste nel dare una classe di appartenenza alla componente di una proposizione Il tipo delle proposizioni: se una componente di una proposizione è vista a sua volta come una proposizione Tipo delle proprietà di una classe: attribuire alla componente della proposizione il tipo delle proprietà su X TIpo delle relazioni su una classe: Attribuirealla componente della proposizione il tipo delle relazioni vinarie su X Tipo delle funzioni su una classe: Attribuire alla componente della proposizione il tipo delle funzioni unarie su X |
| Qual è la negazione di di una proposizione che ha la forma ∃x : T A[x]? | ∀x : T ¬A[x] |
| Qual è la negazione di di una proposizione che ha la forma ∀x : T A[x]? | ∃x : T ¬A[x] |
| Come si può dimostrare una proposizione che ha la forma ∃x : T A[x]? | bisogna stabilire la verità di una sua istanza, tramite la dimostrazione |
| Come si può dimostrare una proposizione che ha la forma ∀x : T A[x]? | Per stabilire la verità di una proposizione quantificata universalmente dobbiamo stabilire che tutte le sue istanze sono vere, per le istanze infinite si procede con questa formula dimostrazione di A[a : T] a generico --------------------------------------------------- ∀x : T A[x] |
| Come si può usare in una dimostrazione una proposizione che ha la forma ∀x : T A[x]? | mediante la regola del dictum de omni: ciò che è vero per tutti gli oggetti di un tipo è anche vero per ciascun oggetto di quel tipo |
| Come si può usare in una dimostrazione una proposizione che ha la forma ∃x : T A[x]? | ci deve essere un oggetto a di tipo T che fornisce un'istanza vera di quella proposizione quantificata, oltre ad avere le proprietà comuni di un oggetto di T |
| Cos'è il sillogismo BARBARA e cos'è il sillogismo DARII? | i sillogismi sono forme di ragionamento che permettono di concludere una nuova proposizione categorica a partire da due proposizioni categoriche BARBARA da "ogni M è P" e "ogni S è M" si conlude ogni "S è P" DARII da "ogni M è P" e "qualche S è M" si conclude "qualche S è P" |
| Come si scrivono - nella seconda lettura odierna - una proposizione categorica particolare affermativa e la sua negazione? | la seconda lettura odierna di una proposizione categorica particolare affermativa è "qualche P è Q" è "per ogni x : X, se x è P allora x è Q" e la negazione "ogni P non è Q" è "per qualche x : X, se x è P allora x non è Q" |
| Come si scrivono - nella seconda lettura odierna - una proposizione categorica universale affermativa e la sua negazione? | "ogni P è Q" è "per ogni x : X, se x è P allora x è Q" la sua negazione "qualche P non è Q" è "per qualche x : X, x è P e x non è Q" |
| Cos'è una proposizione del primo ordine? | una proposizione del primo ordine è una proposizione che è costituita mediante connettivi e quantificatori a partire da proposizioni semplici prive di concetti logici, parla di un solo tipo di oggetti e ha quantificatori solo su quello stesso tipo di oggetti |
| Cos'è un modello di una formula del primo ordine? Cos'è un contromodello di una formula del primo ordine? | Un modello di una formula del primo ordine A è un'attribuzione di valori per le variabili libere presenti in A che trasforma A in una proposizione vera. Un contromodello di una formula del primo ordine A è una attribuzione di valori per le variabili libere presenti in A che trasforma la formula proposizione falsa |
| ci sono concetti extra-logici nelle formule del primo ordine? | No, poiché le formule del primo ordine sono ottenute dalle proposizioni del primo ordine rimpiazzando tutti i concetti extra-logici con corrispondenti variabili di tipo logico |
| Quando una formula del primo ordine è soddisfacibile? E come viene chiamata la formula che è la negazione di una formula chiamata soddisfacibile? | Sono dette soddisfacibili le formule che per qualche attribuzione di valori alle loro variabili libere si trasformano in proposizioni vere, ossia le formule che hanno almeno un modello. Quando una formula è soddisfacibile, la formula che è la sua negazione è detta FALSITÀ LOGICA. Sono dette Flasità Logiche le formule che diventano proposizioni false per ogni attribuzione di valori alle proprie varibili libere, ossia le formule che non hanno modelli e che quindi hanno solo contromodelli |
| Quando una formula del primo ordine è una verità logica? E come viene chiamata la formula che è la negazione di una formula chiamata verità logica? | Quando tutte le proposizioni che si ottengono da essa mediante attribuzione di valori alle variabili libere sono vere. la sua negazione è detta falsificabile |
| Quando una formula [A] è conseguenza logica di un insieme [M] di formule? | Una formula A è conseguenza logica di un insieme M di formule quando ogni modello di M è modello di A |
| Esponi le linee generali del teorema di completezza della logica del primo ordine | Kurt-Godel: Per ogni formula A del primo ordine, se ∀(A) è vera, allora ∀(A) e A stessa sono dimostrabili logicamente. La dimostrazione di questo teorema richiede -nozione del linguaggio formale del primo ordine -concetto di dimostrazione logica entro il calcolo della logica della logica del primo ordine -concetto di attribuzione di valori alle aree variabili di un alfabeto del primo ordine |
| Esponi le linee generali del teorema di incompletezza di Godel | Non sempre la soddisfacibilità delle formule del primo ordine può essere dimostrata con la pura logica; la soddisfazione di certe formule non può essere stabilita che con dimostrazioni extra-logiche, in cui la logica interagisce con altre discipline. La logica non può essere sempre autonoma |
| La logica riesce a dimostrare con i propri metodi tutte le sue proposizioni vere? | No, poiché Godel ha dimostrato proprio che ci sono proposizioni logiche vere che non possono essere dimostrate logicamente |
| Cosa sono gli insiemi? | Gli insiemi sono le classi che sono ritenuti enti, le classi che possono appartenere a classi, le classi che possono stare a sinistra del simbolo di appartenenza |
| Cos'è il principio di estensionalità delle classi? | ogni classe è determinata soltanto dai suoi elementi e non dalla sua definizione o dalla sua costruzione |
| Cos'è il principio di comprensione? | Afferma che ad ogni proprietà corrisponde almeno una classe. Per ogni proprietà P esiste una classe X |
| Esponi l'antinomia di Russel | La dimostrazione che dal principio di estensionalità, dal principio di comprensione e dal principio che ogni classe è una cosa si ottiene una proposizione falsa è detta antinomia di Russel. l'antinomia di Russel ci porta a distinguere tra le proprietà alle quali corrisponde un insieme e le proprietà alle quali non corrisponde un insieme |
| Cos'è una definizione induttiva di un insieme? | Una definizione induttiva di un insieme X consiste nel definire X come il più piccolo insieme che contiene tutte le cose che si ottengono a partire da un insieme di cose eseguendo illimitatamente certe operazioni. La più semplice definizione induttiva è quella dell'insieme dei numeri naturali |
| Cosa vuol dire che due insiemi sono equipotenti? Mostra due insiemi infiniti che non sono equipotenti | due insiemi X e Y si dicono equipotenti se esiste una corrispondenza biunivoca da X a Y. In altri termini, due insiemi X e Y sono detti equipotenti quando X ha tanti elementi quanti Y. Per sistemi non equipotenti possiamo prendere in considerazione il teorema di Cantor che afferma che nessun insieme, finito o infinito, è equipotente alla sua potenza |
| Quante sono le successioni finite costituite da k bit? | sono esattamente 2ᵏ |
| Quando una funzione è una codificazione di un insieme X? | quando nella funzione viene associato ad ogni elemento dell'insieme X un numero che è detto codice di quell'elemento, la funzione deve avere le seguenti priorità: essere totale, iniettiva e dotata di algoritmo |
| Enuncia il teorema che sta alla base della possibilità di rappresentare i numeri naturali in una base n (dove n è un numero naturale maggiore o uguale a 2) | Per ogni numero naturale n maggiore o uguale a due, ogni numero naturale diverso da zero può essere rappresentato in una sola maniera come somma finita di potenze decrescenti di n moltiplicate per coefficienti minori di n |
| Qual è un esempio di codificazione delle successioni finite di numeri naturali? | dalla funzione che, ad ogni successione finita di numeri naturali associa il numero che è ottenuto ponendo ciascuno di quei numeri come esponente del corrispondente numero primo |
| Qual è la definizione di algebra di Boole | qualunque insieme che abbia due elementi speciali a e b, una funzione unaria f e due operazioni binarie g e h, quando valgono le undici proprietà che la contraddistinguono |
| Quali sono gli esempi principali di ciò che è chiamata Algebra di Boole? | I principali esempi di Algebra di Boole sono i valori di verità (con le operazioni di congiunzione, disgiunzione e negazione) e la potenza di un insieme (con le operazioni di intersezione, unione e complemento) |
| Quanti sono i possibili connettivi binari? e quanti sono i possibili connettivi n-ari? | i possibili connettivi binari sono 2⁴ ossia 16; i possibili connettivi n-ari sono 2ⁿ |
| mediante la congiunzione classica, la disgiunzione classica e la negazione classica si possono definire tutte le possibili operazioni sui bit? | sì, come è ricordato nell'introduzione e nella parte conclusiva del capitolo, ogni possibile operazione sui bit - e dunque ogni possibile connettivo proposizionale - può essere definita mediante la congiunzione classica e la negazione classica |
| La macchina di Turing è il modello della nostra mente? | No, non è e non può essere il modello logico-matematico della mente umana poiché la nostra mente sa compiere molto più che i soli calcoli. Può essere paragonata a ciò che avviene nella mente umana quando essa compie calcoli senza interazioni o collaborazioni, ossia quando si comporta meccanicamente e da sola |
| Cosa è una istruzione di una macchina di Turing? Cosa è un programma di una macchina di Turing? | Durante l'attività di calcolo di Turing, esegue le operazioni che sa compiere soltanto se e quando esse sono prescritte; una prescrizione di eseguire una o più operazioni è detta istruzione. Le istruzioni per una attività di calcolo devono appartenere a un insieme finito di istruzioni detto programma |
| Quando sono uguali due MdT? | Quando hanno lo stesso programma e quindi lo stesso insieme di stati |
| cos'è una computazione di una MdT? | Una computazione di una MdT è una successione di configurazioni, nella quale: -la prima configurazione è una configurazione iniziale -ciascuna configurazione (eccetto la prima) è ricavata immediatamente da quella precedente eseguendo una istruzione di quella Macchina di Turing -ciascuna configurazione che non sia finale è seguita da una configurazione che si ricava immediatamente da essa |
| Quando una Macchina di Turing è una macchina per una funzione numerica unaria? E quando è una macchina per una funzione numerica k-aria? | Le MdT permettono di calcolare funzioni numeriche. La MdT può calcolare una funzione numerica f unaria quando per ogni numero naturale n la computazione della Macchina M che inizia con la configurazione iniziale costituita dal nastro su cui è rappresentato il numero n ha questa caratteristica: se f(n) è definito, allora la computazione termina in un numero finito di passi con la configurazione finale in cui sul nastro è rappresentato il valore di f(n) -se f(n) non è definito, allora la computazione non termina mai, è infinita La MdT M per una funzione k-aria è quando k-pla ordinata di numeri naturali <n₁,...,nₖ> la computazione della Macchina M che inizia con la configurazione iniziale costituita dal nastro su cui è rappresentato la k-pla ordinata <n₁,...,nₖ> ha questa caratteristica: -se f(n₁,...,nₖ) è definito, allora la computazione termina in un numero finito di passi con la configurazione finale in cui sul nastro è rappresentato il valore f(n₁,...,nₖ) -se f(n₁,...,nₖ) non è definito, allora la computazione non termina mai, è infinita |
| Spiegare e commentare la Tesi di Church | "Ogni funzione numerica calcolabile è Turing-calcolabile". Calcolabile cioè mediante una macchina di Turing. Questa proposizione non potrà mai essere dimostrata rigorosamente, perché per dimostrarla rigorosamente dovremmo far appello al concetto di "macchina possibile" o a quello di "algoritmo possibile", concetti che però sono vaghi e non rigorosi |
| Ci sono funzioni non-calcolabili? e perché? | sì, la teoria delle macchine di turing permette di scoprire anche esempi di funzioni che non sono Turing-calcolabili e quindi - per la tesi di Church - non sono calcolabili, e di concludere in questa maniera che esistono funzioni non calcolabili senza far ricorso a considerazioni sull'infinito |
| Quando una macchina di Turing è deterministica? | è deterministica quando nel suo programma non ci sono istruzioni diverse ma con la stessa condizione, cioè non ci sono istruzioni che dicono di compiere operazioni diverse nello stesso stato e sotto la ostessa lettura della casella dove è posizionata |
| Quali sono le principali assiomatizzazioni della logica del primo ordine? | le principali assiomatizzazioni della logica del primo ordine sono quella data da D.Hilbert e quella data - utilizzando la nozione di sequente - da G. Gentzen |
| Le dimostrazioni logiche si devono svolgere sempre all'interno di un prefissato formalismo? | la risposta è negativa |
| Quali sono gli assiomi e le regole di derivazione, nella assiomatizzazione delle formule che sono verità logiche del primo ordine? | Assioma e regola sulla negazione(detti anche basilari) regole caratteristiche della logica classica(dette anche regole strutturali) assiomi e regole per il vero e il falso regole per la congiunzione e la disgiunzione regole per la quantificazione universale e la quantificazione esistenziale |
| Come sono definiti i sequenti derivabili nel calcolo dei sequenti per la logica del primo ordine? | è anch'esso un sequente derivabile nel calcolo dei sequenti del primo ordine. Se un sequente è ottenuto da due sequenti derivabili nel calcolo dei sequenti del primo ordine allora è anch'esso un sequente derivabile nel calcolo dei sequenti del primo ordine |
| Come è definito un linguaggio formale del primo ordine? | Un linguaggio del primo ordine è caratterizzato da: un alfabeto di simboli (che siano simboli rappresentanti variabili, costanti, predicati, funzioni, connettivi, quantificatori o punteggiatura); un insieme di termini (che denotano gli "oggetti" dell'insieme che si sta considerando); un insieme di formule ben formate (o più brevemente fbf o semplicemente "formule") cioè un insieme di stringhe composte di simboli dell'alfabeto che vengono considerate sintatticamente corrette. |
| È decidibile la proprietà di essere una formula derivabile (o un sequente derivabile) nella logica del primo ordine? | la risposta è negativa, |
| La logica è strumento in ogni disciplina? Ed è possibile ricondurre ogni disciplina alla sola logica? | La logica è strumento di ogni disciplina per sua stessa natura, ma (per il teorema di incompletezza di Gӧdel) non è accettabile la tesi logicistica che ogni disciplina possa essere ricondotta alla logica |
| La logica matematica è parte della filosofia, o lo è soltanto la logica filosofica? | La logica, anche chiamata logica matematica, è parte della filosofia in quanto le questioni della logica compaiono anche nella filosofia e viceversa |
| Mostra alcune ragioni per le quali la logica è base della filosofia della scienza | -Quando nella filosofia della scienza di fa riferimento alle proposizioni di una teoria scientifica, tali proposizioni sono analizzate usando i connettivi e i quantificatori -nell'ambito del positivismo logico, una teoria scientifica viene considerata come qualcosa che è una teoria assiomatica con un linguaggio formalizzato -la logica del primo ordine è la parte della logica che nella filosofia della scienza del '900 è più considerata ed apprezzata anche perché in essa vale il teorema della completezza |
| Quali sono i principali approcci nell'indagine sui fondamenti delle scienze nella seconda metà dell'ottocento e del novecento? | L'approccio Logicista (concetti della scienza definiti in maniera logica, proposizioni della scienza = proposizioni logiche) L'approccio costruttivista (la ricerca sui fondamenti di una scienza consiste nell'accertare quali parti di essa hanno un carattere costruttivo rigettando il resto che non corrisponde al criterio di costruttività) L'approccio Kantiano (La ricerca filosofica sui fondamenti di una scienza consiste nell'indagine sulle condizioni di possibilità di tale scienza, base della matematica di Hilbert) |
| Quali sono le principali branche della logica matematica? | le branche principali della logica matematica sono la teoria della dimostrazione, la teoria dei modelli, la teoria degli insiemi e la teoria della calcolabilità |
| Quali sono le principali nozioni di programma fornite dalla logica all'informatica? | Le principali nozioni di programma, fornite dalla logica all'informatica sono. quella presente nella nozione di Macchina di Turing, quella alla base della programmazione Funzionale e quella alla base della programmazione Logica |
| Cos'è la corrispondenza di Curry-Howard? | è una corrispondenza tra proposizioni e tipi di oggetti, tra dimostrazioni logiche e programmi, tra eliminazione dei tagli ed esecuzione dei programmi |
| Cos'è il calcolo Sintattico di Lambek | il Calcolo Sintattico di Lambek dice che la correttezza sintattica delle espressioni di una lingua naturale corrisponde alla dimostrabilità logica della categoria di quell'espressione, partendo dalle categorie delle sue componenti più semplici una vola che le categorie delle espressioni di quella lingua sono stati espresse mediante formule proposizionali a partire dalla categoria N dei nomi e della categoria E degli enunciati |
Want to create your own Flashcards for free with GoConqr? Learn more.